Theorem aceq5lem3 3560

Description: Lemma for aceq5 3563.

Hypothesis

Ref	Expression
aceq5lem.1	⊢ A = {u∣(¬ u = ∅ ∧ ∃t ∈ h u = ({t} × t))}

Assertion

Ref	Expression
aceq5lem3	⊢ (({w} × w) ∈ A ↔ (¬ w = ∅ ∧ w ∈ h))

Distinct variable group(s):   w,u,t,h   w,A

Proof of Theorem aceq5lem3

Step	Hyp	Ref	Expression
1		snex 1859	. . . 4 ⊢ {w} ∈ V
2		visset 1350	. . . 4 ⊢ w ∈ V
3	1, 2	xpex 2488	. . 3 ⊢ ({w} × w) ∈ V
4		cleq1 1107	. . . . 5 ⊢ (u = ({w} × w) → (u = ∅ ↔ ({w} × w) = ∅))
5	4	negbid 463	. . . 4 ⊢ (u = ({w} × w) → (¬ u = ∅ ↔ ¬ ({w} × w) = ∅))
6		cleq1 1107	. . . . 5 ⊢ (u = ({w} × w) → (u = ({t} × t) ↔ ({w} × w) = ({t} × t)))
7	6	birexdv 1220	. . . 4 ⊢ (u = ({w} × w) → (∃t ∈ h u = ({t} × t) ↔ ∃t ∈ h ({w} × w) = ({t} × t)))
8	5, 7	anbi12d 476	. . 3 ⊢ (u = ({w} × w) → ((¬ u = ∅ ∧ ∃t ∈ h u = ({t} × t)) ↔ (¬ ({w} × w) = ∅ ∧ ∃t ∈ h ({w} × w) = ({t} × t))))
9	3, 8	elab 1415	. 2 ⊢ (({w} × w) ∈ {u∣(¬ u = ∅ ∧ ∃t ∈ h u = ({t} × t))} ↔ (¬ ({w} × w) = ∅ ∧ ∃t ∈ h ({w} × w) = ({t} × t)))
10		aceq5lem.1	. . 3 ⊢ A = {u∣(¬ u = ∅ ∧ ∃t ∈ h u = ({t} × t))}
11	10	eleq2i 1153	. 2 ⊢ (({w} × w) ∈ A ↔ ({w} × w) ∈ {u∣(¬ u = ∅ ∧ ∃t ∈ h u = ({t} × t))})
12		xpeq2 2441	. . . . . 6 ⊢ (w = ∅ → ({w} × w) = ({w} × ∅))
13		xp0 2652	. . . . . 6 ⊢ ({w} × ∅) = ∅
14	12, 13	syl6eq 1140	. . . . 5 ⊢ (w = ∅ → ({w} × w) = ∅)
15		rneq 2555	. . . . . 6 ⊢ (({w} × w) = ∅ → ran ({w} × w) = ran ∅)
16	2	snnz 1846	. . . . . . 7 ⊢ ¬ {w} = ∅
17		rnxp 2657	. . . . . . 7 ⊢ (¬ {w} = ∅ → ran ({w} × w) = w)
18	16, 17	ax-mp 6	. . . . . 6 ⊢ ran ({w} × w) = w
19		rn0 2567	. . . . . 6 ⊢ ran ∅ = ∅
20	15, 18, 19	3eqtr3g 1146	. . . . 5 ⊢ (({w} × w) = ∅ → w = ∅)
21	14, 20	impbi 139	. . . 4 ⊢ (w = ∅ ↔ ({w} × w) = ∅)
22	21	negbii 162	. . 3 ⊢ (¬ w = ∅ ↔ ¬ ({w} × w) = ∅)
23		rneq 2555	. . . . . . . . . . 11 ⊢ (({w} × w) = ({t} × t) → ran ({w} × w) = ran ({t} × t))
24		visset 1350	. . . . . . . . . . . . 13 ⊢ t ∈ V
25	24	snnz 1846	. . . . . . . . . . . 12 ⊢ ¬ {t} = ∅
26		rnxp 2657	. . . . . . . . . . . 12 ⊢ (¬ {t} = ∅ → ran ({t} × t) = t)
27	25, 26	ax-mp 6	. . . . . . . . . . 11 ⊢ ran ({t} × t) = t
28	23, 18, 27	3eqtr3g 1146	. . . . . . . . . 10 ⊢ (({w} × w) = ({t} × t) → w = t)
29		sneq 1816	. . . . . . . . . . . 12 ⊢ (w = t → {w} = {t})
30		xpeq1 2440	. . . . . . . . . . . 12 ⊢ ({w} = {t} → ({w} × w) = ({t} × w))
31	29, 30	syl 12	. . . . . . . . . . 11 ⊢ (w = t → ({w} × w) = ({t} × w))
32		xpeq2 2441	. . . . . . . . . . 11 ⊢ (w = t → ({t} × w) = ({t} × t))
33	31, 32	eqtrd 1128	. . . . . . . . . 10 ⊢ (w = t → ({w} × w) = ({t} × t))
34	28, 33	impbi 139	. . . . . . . . 9 ⊢ (({w} × w) = ({t} × t) ↔ w = t)
35		cleqcom 1103	. . . . . . . . 9 ⊢ (w = t ↔ t = w)
36	34, 35	bitr 151	. . . . . . . 8 ⊢ (({w} × w) = ({t} × t) ↔ t = w)
37	36	anbi2i 367	. . . . . . 7 ⊢ ((t ∈ h ∧ ({w} × w) = ({t} × t)) ↔ (t ∈ h ∧ t = w))
38		ancom 333	. . . . . . 7 ⊢ ((t ∈ h ∧ t = w) ↔ (t = w ∧ t ∈ h))
39	37, 38	bitr 151	. . . . . 6 ⊢ ((t ∈ h ∧ ({w} × w) = ({t} × t)) ↔ (t = w ∧ t ∈ h))
40	39	biex 733	. . . . 5 ⊢ (∃t(t ∈ h ∧ ({w} × w) = ({t} × t)) ↔ ∃t(t = w ∧ t ∈ h))
41		eleq1 1149	. . . . . 6 ⊢ (t = w → (t ∈ h ↔ w ∈ h))
42	2, 41	ceqsexv 1371	. . . . 5 ⊢ (∃t(t = w ∧ t ∈ h) ↔ w ∈ h)
43	40, 42	bitr2 152	. . . 4 ⊢ (w ∈ h ↔ ∃t(t ∈ h ∧ ({w} × w) = ({t} × t)))
44		df-rex 1206	. . . 4 ⊢ (∃t ∈ h ({w} × w) = ({t} × t) ↔ ∃t(t ∈ h ∧ ({w} × w) = ({t} × t)))
45	43, 44	bitr4 154	. . 3 ⊢ (w ∈ h ↔ ∃t ∈ h ({w} × w) = ({t} × t))
46	22, 45	anbi12i 369	. 2 ⊢ ((¬ w = ∅ ∧ w ∈ h) ↔ (¬ ({w} × w) = ∅ ∧ ∃t ∈ h ({w} × w) = ({t} × t)))
47	9, 11, 46	3bitr4 158	1 ⊢ (({w} × w) ∈ A ↔ (¬ w = ∅ ∧ w ∈ h))

Syntax hints:  ¬ wn 1   ↔ wb 127   ∧ wa 196  ∃wex 678   = weq 797   ∈ wel 803  {cab 1090   = wceq 1091   ∈ wcel 1092  ∃wrex 1202  ∅c0 1707  {csn 1808   × cxp 2408  ran crn 2411

This theorem is referenced by:  aceq5lem5 3562

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-6 675  ax-7 676  ax-gen 677  ax-8 798  ax-9 799  ax-10 800  ax-11 801  ax-12 802  ax-13 804  ax-14 805  ax-16 922  ax-17 925  ax-ext 1074  ax-rep 1075  ax-un 1076  ax-pow 1077

This theorem depends on definitions:  df-bi 128  df-or 197  df-an 198  df-ex 679  df-sb 853  df-clab 1093  df-cleq 1097  df-clel 1099  df-ral 1205  df-rex 1206  df-v 1349  df-dif 1489  df-un 1490  df-in 1491  df-ss 1492  df-nul 1708  df-pw 1799  df-sn 1811  df-pr 1812  df-op 1815  df-uni 1920  df-br 2063  df-opab 2098  df-xp 2424  df-rel 2425  df-cnv 2426  df-dm 2428  df-rn 2429

metamath.org