Metamath Proof Explorer

Theorem tz9.12lem3

Description: Lemma for tz9.12 . (Contributed by NM, 22-Sep-2003) (Revised by Mario Carneiro, 11-Sep-2015)

Ref Expression
Hypotheses tz9.12lem.1 ⊢ 𝐴 ∈ V
tz9.12lem.2 ⊢ 𝐹 = ( 𝑧 ∈ V ↦ ∩ { 𝑣 ∈ On ∣ 𝑧 ∈ ( 𝑅1 ‘ 𝑣 ) } )
Assertion tz9.12lem3 ( ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ On 𝑥 ∈ ( 𝑅1 ‘ 𝑦 ) → 𝐴 ∈ ( 𝑅1 ‘ suc suc ∪ ( 𝐹 “ 𝐴 ) ) )

Proof

Step Hyp Ref Expression
1 tz9.12lem.1 ⊢ 𝐴 ∈ V
2 tz9.12lem.2 ⊢ 𝐹 = ( 𝑧 ∈ V ↦ ∩ { 𝑣 ∈ On ∣ 𝑧 ∈ ( 𝑅1 ‘ 𝑣 ) } )
3 2 funmpt2 ⊢ Fun 𝐹
4 fveq2 ⊢ ( 𝑣 = 𝑦 → ( 𝑅1 ‘ 𝑣 ) = ( 𝑅1 ‘ 𝑦 ) )
5 4 eleq2d ⊢ ( 𝑣 = 𝑦 → ( 𝑥 ∈ ( 𝑅1 ‘ 𝑣 ) ↔ 𝑥 ∈ ( 𝑅1 ‘ 𝑦 ) ) )
6 5 rspcev ⊢ ( ( 𝑦 ∈ On ∧ 𝑥 ∈ ( 𝑅1 ‘ 𝑦 ) ) → ∃ 𝑣 ∈ On 𝑥 ∈ ( 𝑅1 ‘ 𝑣 ) )
7 rabn0 ⊢ ( { 𝑣 ∈ On ∣ 𝑥 ∈ ( 𝑅1 ‘ 𝑣 ) } ≠ ∅ ↔ ∃ 𝑣 ∈ On 𝑥 ∈ ( 𝑅1 ‘ 𝑣 ) )
8 6 7 sylibr ⊢ ( ( 𝑦 ∈ On ∧ 𝑥 ∈ ( 𝑅1 ‘ 𝑦 ) ) → { 𝑣 ∈ On ∣ 𝑥 ∈ ( 𝑅1 ‘ 𝑣 ) } ≠ ∅ )
9 intex ⊢ ( { 𝑣 ∈ On ∣ 𝑥 ∈ ( 𝑅1 ‘ 𝑣 ) } ≠ ∅ ↔ ∩ { 𝑣 ∈ On ∣ 𝑥 ∈ ( 𝑅1 ‘ 𝑣 ) } ∈ V )
10 8 9 sylib ⊢ ( ( 𝑦 ∈ On ∧ 𝑥 ∈ ( 𝑅1 ‘ 𝑦 ) ) → ∩ { 𝑣 ∈ On ∣ 𝑥 ∈ ( 𝑅1 ‘ 𝑣 ) } ∈ V )
11 vex ⊢ 𝑥 ∈ V
12 eleq1w ⊢ ( 𝑧 = 𝑥 → ( 𝑧 ∈ ( 𝑅1 ‘ 𝑣 ) ↔ 𝑥 ∈ ( 𝑅1 ‘ 𝑣 ) ) )
13 12 rabbidv ⊢ ( 𝑧 = 𝑥 → { 𝑣 ∈ On ∣ 𝑧 ∈ ( 𝑅1 ‘ 𝑣 ) } = { 𝑣 ∈ On ∣ 𝑥 ∈ ( 𝑅1 ‘ 𝑣 ) } )
14 13 inteqd ⊢ ( 𝑧 = 𝑥 → ∩ { 𝑣 ∈ On ∣ 𝑧 ∈ ( 𝑅1 ‘ 𝑣 ) } = ∩ { 𝑣 ∈ On ∣ 𝑥 ∈ ( 𝑅1 ‘ 𝑣 ) } )
15 14 eleq1d ⊢ ( 𝑧 = 𝑥 → ( ∩ { 𝑣 ∈ On ∣ 𝑧 ∈ ( 𝑅1 ‘ 𝑣 ) } ∈ V ↔ ∩ { 𝑣 ∈ On ∣ 𝑥 ∈ ( 𝑅1 ‘ 𝑣 ) } ∈ V ) )
16 2 dmmpt ⊢ dom 𝐹 = { 𝑧 ∈ V ∣ ∩ { 𝑣 ∈ On ∣ 𝑧 ∈ ( 𝑅1 ‘ 𝑣 ) } ∈ V }
17 15 16 elrab2 ⊢ ( 𝑥 ∈ dom 𝐹 ↔ ( 𝑥 ∈ V ∧ ∩ { 𝑣 ∈ On ∣ 𝑥 ∈ ( 𝑅1 ‘ 𝑣 ) } ∈ V ) )
18 11 17 mpbiran ⊢ ( 𝑥 ∈ dom 𝐹 ↔ ∩ { 𝑣 ∈ On ∣ 𝑥 ∈ ( 𝑅1 ‘ 𝑣 ) } ∈ V )
19 10 18 sylibr ⊢ ( ( 𝑦 ∈ On ∧ 𝑥 ∈ ( 𝑅1 ‘ 𝑦 ) ) → 𝑥 ∈ dom 𝐹 )
20 funfvima ⊢ ( ( Fun 𝐹 ∧ 𝑥 ∈ dom 𝐹 ) → ( 𝑥 ∈ 𝐴 → ( 𝐹 ‘ 𝑥 ) ∈ ( 𝐹 “ 𝐴 ) ) )
21 3 19 20 sylancr ⊢ ( ( 𝑦 ∈ On ∧ 𝑥 ∈ ( 𝑅1 ‘ 𝑦 ) ) → ( 𝑥 ∈ 𝐴 → ( 𝐹 ‘ 𝑥 ) ∈ ( 𝐹 “ 𝐴 ) ) )
22 1 2 tz9.12lem2 ⊢ suc ∪ ( 𝐹 “ 𝐴 ) ∈ On
23 1 2 tz9.12lem1 ⊢ ( 𝐹 “ 𝐴 ) ⊆ On
24 onsucuni ⊢ ( ( 𝐹 “ 𝐴 ) ⊆ On → ( 𝐹 “ 𝐴 ) ⊆ suc ∪ ( 𝐹 “ 𝐴 ) )
25 23 24 ax-mp ⊢ ( 𝐹 “ 𝐴 ) ⊆ suc ∪ ( 𝐹 “ 𝐴 )
26 25 sseli ⊢ ( ( 𝐹 ‘ 𝑥 ) ∈ ( 𝐹 “ 𝐴 ) → ( 𝐹 ‘ 𝑥 ) ∈ suc ∪ ( 𝐹 “ 𝐴 ) )
27 r1ord2 ⊢ ( suc ∪ ( 𝐹 “ 𝐴 ) ∈ On → ( ( 𝐹 ‘ 𝑥 ) ∈ suc ∪ ( 𝐹 “ 𝐴 ) → ( 𝑅1 ‘ ( 𝐹 ‘ 𝑥 ) ) ⊆ ( 𝑅1 ‘ suc ∪ ( 𝐹 “ 𝐴 ) ) ) )
28 22 26 27 mpsyl ⊢ ( ( 𝐹 ‘ 𝑥 ) ∈ ( 𝐹 “ 𝐴 ) → ( 𝑅1 ‘ ( 𝐹 ‘ 𝑥 ) ) ⊆ ( 𝑅1 ‘ suc ∪ ( 𝐹 “ 𝐴 ) ) )
29 21 28 syl6 ⊢ ( ( 𝑦 ∈ On ∧ 𝑥 ∈ ( 𝑅1 ‘ 𝑦 ) ) → ( 𝑥 ∈ 𝐴 → ( 𝑅1 ‘ ( 𝐹 ‘ 𝑥 ) ) ⊆ ( 𝑅1 ‘ suc ∪ ( 𝐹 “ 𝐴 ) ) ) )
30 29 imp ⊢ ( ( ( 𝑦 ∈ On ∧ 𝑥 ∈ ( 𝑅1 ‘ 𝑦 ) ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝑅1 ‘ ( 𝐹 ‘ 𝑥 ) ) ⊆ ( 𝑅1 ‘ suc ∪ ( 𝐹 “ 𝐴 ) ) )
31 14 2 fvmptg ⊢ ( ( 𝑥 ∈ V ∧ ∩ { 𝑣 ∈ On ∣ 𝑥 ∈ ( 𝑅1 ‘ 𝑣 ) } ∈ V ) → ( 𝐹 ‘ 𝑥 ) = ∩ { 𝑣 ∈ On ∣ 𝑥 ∈ ( 𝑅1 ‘ 𝑣 ) } )
32 11 31 mpan ⊢ ( ∩ { 𝑣 ∈ On ∣ 𝑥 ∈ ( 𝑅1 ‘ 𝑣 ) } ∈ V → ( 𝐹 ‘ 𝑥 ) = ∩ { 𝑣 ∈ On ∣ 𝑥 ∈ ( 𝑅1 ‘ 𝑣 ) } )
33 9 32 sylbi ⊢ ( { 𝑣 ∈ On ∣ 𝑥 ∈ ( 𝑅1 ‘ 𝑣 ) } ≠ ∅ → ( 𝐹 ‘ 𝑥 ) = ∩ { 𝑣 ∈ On ∣ 𝑥 ∈ ( 𝑅1 ‘ 𝑣 ) } )
34 ssrab2 ⊢ { 𝑣 ∈ On ∣ 𝑥 ∈ ( 𝑅1 ‘ 𝑣 ) } ⊆ On
35 onint ⊢ ( ( { 𝑣 ∈ On ∣ 𝑥 ∈ ( 𝑅1 ‘ 𝑣 ) } ⊆ On ∧ { 𝑣 ∈ On ∣ 𝑥 ∈ ( 𝑅1 ‘ 𝑣 ) } ≠ ∅ ) → ∩ { 𝑣 ∈ On ∣ 𝑥 ∈ ( 𝑅1 ‘ 𝑣 ) } ∈ { 𝑣 ∈ On ∣ 𝑥 ∈ ( 𝑅1 ‘ 𝑣 ) } )
36 34 35 mpan ⊢ ( { 𝑣 ∈ On ∣ 𝑥 ∈ ( 𝑅1 ‘ 𝑣 ) } ≠ ∅ → ∩ { 𝑣 ∈ On ∣ 𝑥 ∈ ( 𝑅1 ‘ 𝑣 ) } ∈ { 𝑣 ∈ On ∣ 𝑥 ∈ ( 𝑅1 ‘ 𝑣 ) } )
37 33 36 eqeltrd ⊢ ( { 𝑣 ∈ On ∣ 𝑥 ∈ ( 𝑅1 ‘ 𝑣 ) } ≠ ∅ → ( 𝐹 ‘ 𝑥 ) ∈ { 𝑣 ∈ On ∣ 𝑥 ∈ ( 𝑅1 ‘ 𝑣 ) } )
38 fveq2 ⊢ ( 𝑦 = ( 𝐹 ‘ 𝑥 ) → ( 𝑅1 ‘ 𝑦 ) = ( 𝑅1 ‘ ( 𝐹 ‘ 𝑥 ) ) )
39 38 eleq2d ⊢ ( 𝑦 = ( 𝐹 ‘ 𝑥 ) → ( 𝑥 ∈ ( 𝑅1 ‘ 𝑦 ) ↔ 𝑥 ∈ ( 𝑅1 ‘ ( 𝐹 ‘ 𝑥 ) ) ) )
40 5 cbvrabv ⊢ { 𝑣 ∈ On ∣ 𝑥 ∈ ( 𝑅1 ‘ 𝑣 ) } = { 𝑦 ∈ On ∣ 𝑥 ∈ ( 𝑅1 ‘ 𝑦 ) }
41 39 40 elrab2 ⊢ ( ( 𝐹 ‘ 𝑥 ) ∈ { 𝑣 ∈ On ∣ 𝑥 ∈ ( 𝑅1 ‘ 𝑣 ) } ↔ ( ( 𝐹 ‘ 𝑥 ) ∈ On ∧ 𝑥 ∈ ( 𝑅1 ‘ ( 𝐹 ‘ 𝑥 ) ) ) )
42 41 simprbi ⊢ ( ( 𝐹 ‘ 𝑥 ) ∈ { 𝑣 ∈ On ∣ 𝑥 ∈ ( 𝑅1 ‘ 𝑣 ) } → 𝑥 ∈ ( 𝑅1 ‘ ( 𝐹 ‘ 𝑥 ) ) )
43 8 37 42 3syl ⊢ ( ( 𝑦 ∈ On ∧ 𝑥 ∈ ( 𝑅1 ‘ 𝑦 ) ) → 𝑥 ∈ ( 𝑅1 ‘ ( 𝐹 ‘ 𝑥 ) ) )
44 43 adantr ⊢ ( ( ( 𝑦 ∈ On ∧ 𝑥 ∈ ( 𝑅1 ‘ 𝑦 ) ) ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ ( 𝑅1 ‘ ( 𝐹 ‘ 𝑥 ) ) )
45 30 44 sseldd ⊢ ( ( ( 𝑦 ∈ On ∧ 𝑥 ∈ ( 𝑅1 ‘ 𝑦 ) ) ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ ( 𝑅1 ‘ suc ∪ ( 𝐹 “ 𝐴 ) ) )
46 45 exp31 ⊢ ( 𝑦 ∈ On → ( 𝑥 ∈ ( 𝑅1 ‘ 𝑦 ) → ( 𝑥 ∈ 𝐴 → 𝑥 ∈ ( 𝑅1 ‘ suc ∪ ( 𝐹 “ 𝐴 ) ) ) ) )
47 46 com3r ⊢ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ On → ( 𝑥 ∈ ( 𝑅1 ‘ 𝑦 ) → 𝑥 ∈ ( 𝑅1 ‘ suc ∪ ( 𝐹 “ 𝐴 ) ) ) ) )
48 47 rexlimdv ⊢ ( 𝑥 ∈ 𝐴 → ( ∃ 𝑦 ∈ On 𝑥 ∈ ( 𝑅1 ‘ 𝑦 ) → 𝑥 ∈ ( 𝑅1 ‘ suc ∪ ( 𝐹 “ 𝐴 ) ) ) )
49 48 ralimia ⊢ ( ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ On 𝑥 ∈ ( 𝑅1 ‘ 𝑦 ) → ∀ 𝑥 ∈ 𝐴 𝑥 ∈ ( 𝑅1 ‘ suc ∪ ( 𝐹 “ 𝐴 ) ) )
50 r1suc ⊢ ( suc ∪ ( 𝐹 “ 𝐴 ) ∈ On → ( 𝑅1 ‘ suc suc ∪ ( 𝐹 “ 𝐴 ) ) = 𝒫 ( 𝑅1 ‘ suc ∪ ( 𝐹 “ 𝐴 ) ) )
51 22 50 ax-mp ⊢ ( 𝑅1 ‘ suc suc ∪ ( 𝐹 “ 𝐴 ) ) = 𝒫 ( 𝑅1 ‘ suc ∪ ( 𝐹 “ 𝐴 ) )
52 51 eleq2i ⊢ ( 𝐴 ∈ ( 𝑅1 ‘ suc suc ∪ ( 𝐹 “ 𝐴 ) ) ↔ 𝐴 ∈ 𝒫 ( 𝑅1 ‘ suc ∪ ( 𝐹 “ 𝐴 ) ) )
53 1 elpw ⊢ ( 𝐴 ∈ 𝒫 ( 𝑅1 ‘ suc ∪ ( 𝐹 “ 𝐴 ) ) ↔ 𝐴 ⊆ ( 𝑅1 ‘ suc ∪ ( 𝐹 “ 𝐴 ) ) )
54 dfss3 ⊢ ( 𝐴 ⊆ ( 𝑅1 ‘ suc ∪ ( 𝐹 “ 𝐴 ) ) ↔ ∀ 𝑥 ∈ 𝐴 𝑥 ∈ ( 𝑅1 ‘ suc ∪ ( 𝐹 “ 𝐴 ) ) )
55 52 53 54 3bitri ⊢ ( 𝐴 ∈ ( 𝑅1 ‘ suc suc ∪ ( 𝐹 “ 𝐴 ) ) ↔ ∀ 𝑥 ∈ 𝐴 𝑥 ∈ ( 𝑅1 ‘ suc ∪ ( 𝐹 “ 𝐴 ) ) )
56 49 55 sylibr ⊢ ( ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ On 𝑥 ∈ ( 𝑅1 ‘ 𝑦 ) → 𝐴 ∈ ( 𝑅1 ‘ suc suc ∪ ( 𝐹 “ 𝐴 ) ) )