Metamath Proof Explorer

Metamath Proof Explorer

< Previous Next >
Related theorems
GIF version

Theorem tz9.12lem3 3505

Description: Lemma for tz9.12 3506.

**Hypotheses**
Ref	Expression
tz9.12lem.1	⊢ A ∈ V
tz9.12lem.2	⊢ F = {⟨z, w⟩∣w = ∩{v ∈ On∣z ∈ (R₁ ‘v)}}

**Assertion**
Ref	Expression
tz9.12lem3	⊢ (∀x ∈ A ∃y ∈ On x ∈ (R₁ ‘y) → A ∈ (R₁ ‘suc suc ∪(F “ A)))

Distinct variable group(s): x,y,z,w,v,A x,F,y

**Proof of Theorem tz9.12lem3**
Step	Hyp	Ref	Expression
1		fveq2 2832	. . . . . . . . . . . . . 14 ⊢ (v = y → (R₁ ‘v) = (R₁ ‘y))
2	1	eleq2d 1156	. . . . . . . . . . . . 13 ⊢ (v = y → (x ∈ (R₁ ‘v) ↔ x ∈ (R₁ ‘y)))
3	2	rcla4ev 1403	. . . . . . . . . . . 12 ⊢ ((y ∈ On ∧ x ∈ (R₁ ‘y)) → ∃v ∈ On x ∈ (R₁ ‘v))
4		rabn0 1716	. . . . . . . . . . . 12 ⊢ (¬ {v ∈ On∣x ∈ (R₁ ‘v)} = ∅ ↔ ∃v ∈ On x ∈ (R₁ ‘v))
5	3, 4	sylibr 175	. . . . . . . . . . 11 ⊢ ((y ∈ On ∧ x ∈ (R₁ ‘y)) → ¬ {v ∈ On∣x ∈ (R₁ ‘v)} = ∅)
6		tz9.12lem.2	. . . . . . . . . . . . . . . 16 ⊢ F = {⟨z, w⟩∣w = ∩{v ∈ On∣z ∈ (R₁ ‘v)}}
7	6	eleq2i 1153	. . . . . . . . . . . . . . 15 ⊢ (⟨x, y⟩ ∈ F ↔ ⟨x, y⟩ ∈ {⟨z, w⟩∣w = ∩{v ∈ On∣z ∈ (R₁ ‘v)}})
8		visset 1350	. . . . . . . . . . . . . . . 16 ⊢ x ∈ V
9		visset 1350	. . . . . . . . . . . . . . . 16 ⊢ y ∈ V
10		eleq1 1149	. . . . . . . . . . . . . . . . . . 19 ⊢ (z = x → (z ∈ (R₁ ‘v) ↔ x ∈ (R₁ ‘v)))
11	10	birabsdv 1344	. . . . . . . . . . . . . . . . . 18 ⊢ (z = x → {v ∈ On∣z ∈ (R₁ ‘v)} = {v ∈ On∣x ∈ (R₁ ‘v)})
12	11	inteqd 1970	. . . . . . . . . . . . . . . . 17 ⊢ (z = x → ∩{v ∈ On∣z ∈ (R₁ ‘v)} = ∩{v ∈ On∣x ∈ (R₁ ‘v)})
13	12	cleq2d 1112	. . . . . . . . . . . . . . . 16 ⊢ (z = x → (w = ∩{v ∈ On∣z ∈ (R₁ ‘v)} ↔ w = ∩{v ∈ On∣x ∈ (R₁ ‘v)}))
14		cleq1 1107	. . . . . . . . . . . . . . . 16 ⊢ (w = y → (w = ∩{v ∈ On∣x ∈ (R₁ ‘v)} ↔ y = ∩{v ∈ On∣x ∈ (R₁ ‘v)}))
15	8, 9, 13, 14	opelopab 2117	. . . . . . . . . . . . . . 15 ⊢ (⟨x, y⟩ ∈ {⟨z, w⟩∣w = ∩{v ∈ On∣z ∈ (R₁ ‘v)}} ↔ y = ∩{v ∈ On∣x ∈ (R₁ ‘v)})
16	7, 15	bitr 151	. . . . . . . . . . . . . 14 ⊢ (⟨x, y⟩ ∈ F ↔ y = ∩{v ∈ On∣x ∈ (R₁ ‘v)})
17	16	biex 733	. . . . . . . . . . . . 13 ⊢ (∃y⟨x, y⟩ ∈ F ↔ ∃y y = ∩{v ∈ On∣x ∈ (R₁ ‘v)})
18	8	eldm2 2528	. . . . . . . . . . . . 13 ⊢ (x ∈ dom F ↔ ∃y⟨x, y⟩ ∈ F)
19		isset 1351	. . . . . . . . . . . . 13 ⊢ (∩{v ∈ On∣x ∈ (R₁ ‘v)} ∈ V ↔ ∃y y = ∩{v ∈ On∣x ∈ (R₁ ‘v)})
20	17, 18, 19	3bitr4 158	. . . . . . . . . . . 12 ⊢ (x ∈ dom F ↔ ∩{v ∈ On∣x ∈ (R₁ ‘v)} ∈ V)
21		intex 1986	. . . . . . . . . . . 12 ⊢ (¬ {v ∈ On∣x ∈ (R₁ ‘v)} = ∅ ↔ ∩{v ∈ On∣x ∈ (R₁ ‘v)} ∈ V)
22	20, 21	bitr4 154	. . . . . . . . . . 11 ⊢ (x ∈ dom F ↔ ¬ {v ∈ On∣x ∈ (R₁ ‘v)} = ∅)
23	5, 22	sylibr 175	. . . . . . . . . 10 ⊢ ((y ∈ On ∧ x ∈ (R₁ ‘y)) → x ∈ dom F)
24		funopabeq 2695	. . . . . . . . . . . 12 ⊢ Fun {⟨z, w⟩∣w = ∩{v ∈ On∣z ∈ (R₁ ‘v)}}
25		funeq 2683	. . . . . . . . . . . . 13 ⊢ (F = {⟨z, w⟩∣w = ∩{v ∈ On∣z ∈ (R₁ ‘v)}} → (Fun F ↔ Fun {⟨z, w⟩∣w = ∩{v ∈ On∣z ∈ (R₁ ‘v)}}))
26	6, 25	ax-mp 6	. . . . . . . . . . . 12 ⊢ (Fun F ↔ Fun {⟨z, w⟩∣w = ∩{v ∈ On∣z ∈ (R₁ ‘v)}})
27	24, 26	mpbir 165	. . . . . . . . . . 11 ⊢ Fun F
28		funfvima 2904	. . . . . . . . . . 11 ⊢ ((Fun F ∧ x ∈ dom F) → (x ∈ A → (F ‘x) ∈ (F “ A)))
29	27, 28	mpan 518	. . . . . . . . . 10 ⊢ (x ∈ dom F → (x ∈ A → (F ‘x) ∈ (F “ A)))
30	23, 29	syl 12	. . . . . . . . 9 ⊢ ((y ∈ On ∧ x ∈ (R₁ ‘y)) → (x ∈ A → (F ‘x) ∈ (F “ A)))
31		tz9.12lem.1	. . . . . . . . . . . . 13 ⊢ A ∈ V
32	31, 6	tz9.12lem1 3503	. . . . . . . . . . . 12 ⊢ (F “ A) ⊆ On
33		onsucuni 2335	. . . . . . . . . . . 12 ⊢ ((F “ A) ⊆ On → (F “ A) ⊆ suc ∪(F “ A))
34	32, 33	ax-mp 6	. . . . . . . . . . 11 ⊢ (F “ A) ⊆ suc ∪(F “ A)
35	34	sseli 1504	. . . . . . . . . 10 ⊢ ((F ‘x) ∈ (F “ A) → (F ‘x) ∈ suc ∪(F “ A))
36	31, 6	tz9.12lem2 3504	. . . . . . . . . . 11 ⊢ suc ∪(F “ A) ∈ On
37		r1ord2 3500	. . . . . . . . . . 11 ⊢ (suc ∪(F “ A) ∈ On → ((F ‘x) ∈ suc ∪(F “ A) → (R₁ ‘(F ‘x)) ⊆ (R₁ ‘suc ∪(F “ A))))
38	36, 37	ax-mp 6	. . . . . . . . . 10 ⊢ ((F ‘x) ∈ suc ∪(F “ A) → (R₁ ‘(F ‘x)) ⊆ (R₁ ‘suc ∪(F “ A)))
39	35, 38	syl 12	. . . . . . . . 9 ⊢ ((F ‘x) ∈ (F “ A) → (R₁ ‘(F ‘x)) ⊆ (R₁ ‘suc ∪(F “ A)))
40	30, 39	syl6 23	. . . . . . . 8 ⊢ ((y ∈ On ∧ x ∈ (R₁ ‘y)) → (x ∈ A → (R₁ ‘(F ‘x)) ⊆ (R₁ ‘suc ∪(F “ A))))
41	40	imp 277	. . . . . . 7 ⊢ (((y ∈ On ∧ x ∈ (R₁ ‘y)) ∧ x ∈ A) → (R₁ ‘(F ‘x)) ⊆ (R₁ ‘suc ∪(F “ A)))
42	12	fvopabg 2872	. . . . . . . . . . . . 13 ⊢ ((x ∈ V ∧ ∩{v ∈ On∣x ∈ (R₁ ‘v)} ∈ V) → ({⟨z, w⟩∣w = ∩{v ∈ On∣z ∈ (R₁ ‘v)}} ‘x) = ∩{v ∈ On∣x ∈ (R₁ ‘v)})
43	8, 42	mpan 518	. . . . . . . . . . . 12 ⊢ (∩{v ∈ On∣x ∈ (R₁ ‘v)} ∈ V → ({⟨z, w⟩∣w = ∩{v ∈ On∣z ∈ (R₁ ‘v)}} ‘x) = ∩{v ∈ On∣x ∈ (R₁ ‘v)})
44	6	fveq1i 2833	. . . . . . . . . . . 12 ⊢ (F ‘x) = ({⟨z, w⟩∣w = ∩{v ∈ On∣z ∈ (R₁ ‘v)}} ‘x)
45	43, 44	syl5eq 1136	. . . . . . . . . . 11 ⊢ (∩{v ∈ On∣x ∈ (R₁ ‘v)} ∈ V → (F ‘x) = ∩{v ∈ On∣x ∈ (R₁ ‘v)})
46	21, 45	sylbi 174	. . . . . . . . . 10 ⊢ (¬ {v ∈ On∣x ∈ (R₁ ‘v)} = ∅ → (F ‘x) = ∩{v ∈ On∣x ∈ (R₁ ‘v)})
47		ssrab 1556	. . . . . . . . . . 11 ⊢ {v ∈ On∣x ∈ (R₁ ‘v)} ⊆ On
48		onint 2261	. . . . . . . . . . 11 ⊢ (({v ∈ On∣x ∈ (R₁ ‘v)} ⊆ On ∧ ¬ {v ∈ On∣x ∈ (R₁ ‘v)} = ∅) → ∩{v ∈ On∣x ∈ (R₁ ‘v)} ∈ {v ∈ On∣x ∈ (R₁ ‘v)})
49	47, 48	mpan 518	. . . . . . . . . 10 ⊢ (¬ {v ∈ On∣x ∈ (R₁ ‘v)} = ∅ → ∩{v ∈ On∣x ∈ (R₁ ‘v)} ∈ {v ∈ On∣x ∈ (R₁ ‘v)})
50	46, 49	eqeltrd 1163	. . . . . . . . 9 ⊢ (¬ {v ∈ On∣x ∈ (R₁ ‘v)} = ∅ → (F ‘x) ∈ {v ∈ On∣x ∈ (R₁ ‘v)})
51		hbrab1 1310	. . . . . . . . . . . . . . . 16 ⊢ (w ∈ {v ∈ On∣z ∈ (R₁ ‘v)} → ∀v w ∈ {v ∈ On∣z ∈ (R₁ ‘v)})
52	51	hbint 1975	. . . . . . . . . . . . . . 15 ⊢ (w ∈ ∩{v ∈ On∣z ∈ (R₁ ‘v)} → ∀v w ∈ ∩{v ∈ On∣z ∈ (R₁ ‘v)})
53	52	hbeleq 1173	. . . . . . . . . . . . . 14 ⊢ (w = ∩{v ∈ On∣z ∈ (R₁ ‘v)} → ∀v w = ∩{v ∈ On∣z ∈ (R₁ ‘v)})
54	53	hbopab 2111	. . . . . . . . . . . . 13 ⊢ (y ∈ {⟨z, w⟩∣w = ∩{v ∈ On∣z ∈ (R₁ ‘v)}} → ∀v y ∈ {⟨z, w⟩∣w = ∩{v ∈ On∣z ∈ (R₁ ‘v)}})
55	6	eleq2i 1153	. . . . . . . . . . . . 13 ⊢ (y ∈ F ↔ y ∈ {⟨z, w⟩∣w = ∩{v ∈ On∣z ∈ (R₁ ‘v)}})
56	55	bial 695	. . . . . . . . . . . . 13 ⊢ (∀v y ∈ F ↔ ∀v y ∈ {⟨z, w⟩∣w = ∩{v ∈ On∣z ∈ (R₁ ‘v)}})
57	54, 55, 56	3imtr4 192	. . . . . . . . . . . 12 ⊢ (y ∈ F → ∀v y ∈ F)
58		ax-17 925	. . . . . . . . . . . 12 ⊢ (y ∈ x → ∀v y ∈ x)
59	57, 58	hbfv 2837	. . . . . . . . . . 11 ⊢ (y ∈ (F ‘x) → ∀v y ∈ (F ‘x))
60		ax-17 925	. . . . . . . . . . 11 ⊢ (y ∈ On → ∀v y ∈ On)
61		ax-17 925	. . . . . . . . . . . . 13 ⊢ (y ∈ R₁ → ∀v y ∈ R₁)
62	61, 59	hbfv 2837	. . . . . . . . . . . 12 ⊢ (y ∈ (R₁ ‘(F ‘x)) → ∀v y ∈ (R₁ ‘(F ‘x)))
63	58, 62	hbel 1172	. . . . . . . . . . 11 ⊢ (x ∈ (R₁ ‘(F ‘x)) → ∀v x ∈ (R₁ ‘(F ‘x)))
64		fveq2 2832	. . . . . . . . . . . 12 ⊢ (v = (F ‘x) → (R₁ ‘v) = (R₁ ‘(F ‘x)))
65	64	eleq2d 1156	. . . . . . . . . . 11 ⊢ (v = (F ‘x) → (x ∈ (R₁ ‘v) ↔ x ∈ (R₁ ‘(F ‘x))))
66	59, 60, 63, 65	elrabf 1421	. . . . . . . . . 10 ⊢ ((F ‘x) ∈ {v ∈ On∣x ∈ (R₁ ‘v)} ↔ ((F ‘x) ∈ On ∧ x ∈ (R₁ ‘(F ‘x))))
67	66	pm3.27bd 263	. . . . . . . . 9 ⊢ ((F ‘x) ∈ {v ∈ On∣x ∈ (R₁ ‘v)} → x ∈ (R₁ ‘(F ‘x)))
68	5, 50, 67	3syl 21	. . . . . . . 8 ⊢ ((y ∈ On ∧ x ∈ (R₁ ‘y)) → x ∈ (R₁ ‘(F ‘x)))
69	68	adantr 306	. . . . . . 7 ⊢ (((y ∈ On ∧ x ∈ (R₁ ‘y)) ∧ x ∈ A) → x ∈ (R₁ ‘(F ‘x)))
70	41, 69	sseldd 1507	. . . . . 6 ⊢ (((y ∈ On ∧ x ∈ (R₁ ‘y)) ∧ x ∈ A) → x ∈ (R₁ ‘suc ∪(F “ A)))
71	70	exp31 293	. . . . 5 ⊢ (y ∈ On → (x ∈ (R₁ ‘y) → (x ∈ A → x ∈ (R₁ ‘suc ∪(F “ A)))))
72	71	com3r 35	. . . 4 ⊢ (x ∈ A → (y ∈ On → (x ∈ (R₁ ‘y) → x ∈ (R₁ ‘suc ∪(F “ A)))))
73	72	r19.23adv 1286	. . 3 ⊢ (x ∈ A → (∃y ∈ On x ∈ (R₁ ‘y) → x ∈ (R₁ ‘suc ∪(F “ A))))
74	73	r19.20i 1253	. 2 ⊢ (∀x ∈ A ∃y ∈ On x ∈ (R₁ ‘y) → ∀x ∈ A x ∈ (R₁ ‘suc ∪(F “ A)))
75		r1suc 3496	. . . . 5 ⊢ (suc ∪(F “ A) ∈ On → (R₁ ‘suc suc ∪(F “ A)) = ℘(R₁ ‘suc ∪(F “ A)))
76	36, 75	ax-mp 6	. . . 4 ⊢ (R₁ ‘suc suc ∪(F “ A)) = ℘(R₁ ‘suc ∪(F “ A))
77	76	eleq2i 1153	. . 3 ⊢ (A ∈ (R₁ ‘suc suc ∪(F “ A)) ↔ A ∈ ℘(R₁ ‘suc ∪(F “ A)))
78	31	elpw 1801	. . 3 ⊢ (A ∈ ℘(R₁ ‘suc ∪(F “ A)) ↔ A ⊆ (R₁ ‘suc ∪(F “ A)))
79		dfss3 1498	. . 3 ⊢ (A ⊆ (R₁ ‘suc ∪(F “ A)) ↔ ∀x ∈ A x ∈ (R₁ ‘suc ∪(F “ A)))
80	77, 78, 79	3bitr 155	. 2 ⊢ (A ∈ (R₁ ‘suc suc ∪(F “ A)) ↔ ∀x ∈ A x ∈ (R₁ ‘suc ∪(F “ A)))
81	74, 80	sylibr 175	1 ⊢ (∀x ∈ A ∃y ∈ On x ∈ (R₁ ‘y) → A ∈ (R₁ ‘suc suc ∪(F “ A)))

Colors of variables: wff set class

Syntax hints: ¬ wn 1 → wi 2 ↔ wb 127 ∧ wa 196 ∀wal 672 ∃wex 678 = weq 797 ∈ wel 803 = wceq 1091 ∈ wcel 1092 ∀wral 1201 ∃wrex 1202 {crab 1204 Vcvv 1348 ⊆ wss 1487 ∅c0 1707 ℘cpw 1798 ⟨cop 1810 ∪cuni 1919 ∩cint 1965 {copab 2055 Oncon0 2199 suc csuc 2201 dom cdm 2410 “ cima 2413 Fun wfun 2416 ‘cfv 2422 R₁cr1 3485

This theorem is referenced by: tz9.12 3506

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-3or 582 df-3an 583 df-ex 679 df-sb 853 df-eu 1009 df-mo 1010 df-clab 1093 df-cleq 1097 df-clel 1099 df-ral 1205 df-rex 1206 df-rab 1208 df-v 1349 df-sbc 1441 df-dif 1489 df-un 1490 df-in 1491 df-ss 1492 df-nul 1708 df-if 1777 df-pw 1799 df-sn 1811 df-pr 1812 df-tp 1814 df-op 1815 df-uni 1920 df-int 1966 df-iun 1996 df-tr 2042 df-br 2063 df-opab 2098 df-eprel 2122 df-id 2125 df-po 2128 df-so 2138 df-fr 2169 df-we 2186 df-ord 2202 df-on 2203 df-lim 2204 df-suc 2205 df-xp 2424 df-rel 2425 df-cnv 2426 df-co 2427 df-dm 2428 df-rn 2429 df-res 2430 df-ima 2431 df-fun 2432 df-fn 2433 df-fv 2438 df-rdg 2970 df-r1 3487

metamath.org