Metamath Proof Explorer

Theorem tz9.1regs

Description: Every set has a transitive closure (the smallest transitive extension). This version of tz9.1 depends on ax-regs instead of ax-reg and ax-inf2 . This suggests a possible answer to the third question posed in tz9.1 , namely that the missing property is that countably infinite classes must obey regularity. In ZF set theory we can prove this by showing that countably infinite classes are sets and thus ax-reg applies to them directly, but in a finitist context it seems that an axiom like ax-regs is required since countably infinite classes are proper classes. (Contributed by BTernaryTau, 31-Dec-2025)

Ref Expression
Hypothesis tz9.1regs.1 ⊢ 𝐴 ∈ V
Assertion tz9.1regs ∃ 𝑥 ( 𝐴 ⊆ 𝑥 ∧ Tr 𝑥 ∧ ∀ 𝑦 ( ( 𝐴 ⊆ 𝑦 ∧ Tr 𝑦 ) → 𝑥 ⊆ 𝑦 ) )

Proof

Step Hyp Ref Expression
1 tz9.1regs.1 ⊢ 𝐴 ∈ V
2 sseq1 ⊢ ( 𝑧 = 𝐴 → ( 𝑧 ⊆ 𝑥 ↔ 𝐴 ⊆ 𝑥 ) )
3 cleq1lem ⊢ ( 𝑧 = 𝐴 → ( ( 𝑧 ⊆ 𝑦 ∧ Tr 𝑦 ) ↔ ( 𝐴 ⊆ 𝑦 ∧ Tr 𝑦 ) ) )
4 3 imbi1d ⊢ ( 𝑧 = 𝐴 → ( ( ( 𝑧 ⊆ 𝑦 ∧ Tr 𝑦 ) → 𝑥 ⊆ 𝑦 ) ↔ ( ( 𝐴 ⊆ 𝑦 ∧ Tr 𝑦 ) → 𝑥 ⊆ 𝑦 ) ) )
5 4 albidv ⊢ ( 𝑧 = 𝐴 → ( ∀ 𝑦 ( ( 𝑧 ⊆ 𝑦 ∧ Tr 𝑦 ) → 𝑥 ⊆ 𝑦 ) ↔ ∀ 𝑦 ( ( 𝐴 ⊆ 𝑦 ∧ Tr 𝑦 ) → 𝑥 ⊆ 𝑦 ) ) )
6 2 5 3anbi13d ⊢ ( 𝑧 = 𝐴 → ( ( 𝑧 ⊆ 𝑥 ∧ Tr 𝑥 ∧ ∀ 𝑦 ( ( 𝑧 ⊆ 𝑦 ∧ Tr 𝑦 ) → 𝑥 ⊆ 𝑦 ) ) ↔ ( 𝐴 ⊆ 𝑥 ∧ Tr 𝑥 ∧ ∀ 𝑦 ( ( 𝐴 ⊆ 𝑦 ∧ Tr 𝑦 ) → 𝑥 ⊆ 𝑦 ) ) ) )
7 6 exbidv ⊢ ( 𝑧 = 𝐴 → ( ∃ 𝑥 ( 𝑧 ⊆ 𝑥 ∧ Tr 𝑥 ∧ ∀ 𝑦 ( ( 𝑧 ⊆ 𝑦 ∧ Tr 𝑦 ) → 𝑥 ⊆ 𝑦 ) ) ↔ ∃ 𝑥 ( 𝐴 ⊆ 𝑥 ∧ Tr 𝑥 ∧ ∀ 𝑦 ( ( 𝐴 ⊆ 𝑦 ∧ Tr 𝑦 ) → 𝑥 ⊆ 𝑦 ) ) ) )
8 sseq1 ⊢ ( 𝑧 = 𝑤 → ( 𝑧 ⊆ 𝑥 ↔ 𝑤 ⊆ 𝑥 ) )
9 cleq1lem ⊢ ( 𝑧 = 𝑤 → ( ( 𝑧 ⊆ 𝑦 ∧ Tr 𝑦 ) ↔ ( 𝑤 ⊆ 𝑦 ∧ Tr 𝑦 ) ) )
10 9 imbi1d ⊢ ( 𝑧 = 𝑤 → ( ( ( 𝑧 ⊆ 𝑦 ∧ Tr 𝑦 ) → 𝑥 ⊆ 𝑦 ) ↔ ( ( 𝑤 ⊆ 𝑦 ∧ Tr 𝑦 ) → 𝑥 ⊆ 𝑦 ) ) )
11 10 albidv ⊢ ( 𝑧 = 𝑤 → ( ∀ 𝑦 ( ( 𝑧 ⊆ 𝑦 ∧ Tr 𝑦 ) → 𝑥 ⊆ 𝑦 ) ↔ ∀ 𝑦 ( ( 𝑤 ⊆ 𝑦 ∧ Tr 𝑦 ) → 𝑥 ⊆ 𝑦 ) ) )
12 8 11 3anbi13d ⊢ ( 𝑧 = 𝑤 → ( ( 𝑧 ⊆ 𝑥 ∧ Tr 𝑥 ∧ ∀ 𝑦 ( ( 𝑧 ⊆ 𝑦 ∧ Tr 𝑦 ) → 𝑥 ⊆ 𝑦 ) ) ↔ ( 𝑤 ⊆ 𝑥 ∧ Tr 𝑥 ∧ ∀ 𝑦 ( ( 𝑤 ⊆ 𝑦 ∧ Tr 𝑦 ) → 𝑥 ⊆ 𝑦 ) ) ) )
13 12 exbidv ⊢ ( 𝑧 = 𝑤 → ( ∃ 𝑥 ( 𝑧 ⊆ 𝑥 ∧ Tr 𝑥 ∧ ∀ 𝑦 ( ( 𝑧 ⊆ 𝑦 ∧ Tr 𝑦 ) → 𝑥 ⊆ 𝑦 ) ) ↔ ∃ 𝑥 ( 𝑤 ⊆ 𝑥 ∧ Tr 𝑥 ∧ ∀ 𝑦 ( ( 𝑤 ⊆ 𝑦 ∧ Tr 𝑦 ) → 𝑥 ⊆ 𝑦 ) ) ) )
14 vex ⊢ 𝑧 ∈ V
15 3simpa ⊢ ( ( 𝑤 ⊆ 𝑥 ∧ Tr 𝑥 ∧ ∀ 𝑦 ( ( 𝑤 ⊆ 𝑦 ∧ Tr 𝑦 ) → 𝑥 ⊆ 𝑦 ) ) → ( 𝑤 ⊆ 𝑥 ∧ Tr 𝑥 ) )
16 15 eximi ⊢ ( ∃ 𝑥 ( 𝑤 ⊆ 𝑥 ∧ Tr 𝑥 ∧ ∀ 𝑦 ( ( 𝑤 ⊆ 𝑦 ∧ Tr 𝑦 ) → 𝑥 ⊆ 𝑦 ) ) → ∃ 𝑥 ( 𝑤 ⊆ 𝑥 ∧ Tr 𝑥 ) )
17 intexab ⊢ ( ∃ 𝑥 ( 𝑤 ⊆ 𝑥 ∧ Tr 𝑥 ) ↔ ∩ { 𝑥 ∣ ( 𝑤 ⊆ 𝑥 ∧ Tr 𝑥 ) } ∈ V )
18 16 17 sylib ⊢ ( ∃ 𝑥 ( 𝑤 ⊆ 𝑥 ∧ Tr 𝑥 ∧ ∀ 𝑦 ( ( 𝑤 ⊆ 𝑦 ∧ Tr 𝑦 ) → 𝑥 ⊆ 𝑦 ) ) → ∩ { 𝑥 ∣ ( 𝑤 ⊆ 𝑥 ∧ Tr 𝑥 ) } ∈ V )
19 18 ralimi ⊢ ( ∀ 𝑤 ∈ 𝑧 ∃ 𝑥 ( 𝑤 ⊆ 𝑥 ∧ Tr 𝑥 ∧ ∀ 𝑦 ( ( 𝑤 ⊆ 𝑦 ∧ Tr 𝑦 ) → 𝑥 ⊆ 𝑦 ) ) → ∀ 𝑤 ∈ 𝑧 ∩ { 𝑥 ∣ ( 𝑤 ⊆ 𝑥 ∧ Tr 𝑥 ) } ∈ V )
20 iunexg ⊢ ( ( 𝑧 ∈ V ∧ ∀ 𝑤 ∈ 𝑧 ∩ { 𝑥 ∣ ( 𝑤 ⊆ 𝑥 ∧ Tr 𝑥 ) } ∈ V ) → ∪ 𝑤 ∈ 𝑧 ∩ { 𝑥 ∣ ( 𝑤 ⊆ 𝑥 ∧ Tr 𝑥 ) } ∈ V )
21 14 19 20 sylancr ⊢ ( ∀ 𝑤 ∈ 𝑧 ∃ 𝑥 ( 𝑤 ⊆ 𝑥 ∧ Tr 𝑥 ∧ ∀ 𝑦 ( ( 𝑤 ⊆ 𝑦 ∧ Tr 𝑦 ) → 𝑥 ⊆ 𝑦 ) ) → ∪ 𝑤 ∈ 𝑧 ∩ { 𝑥 ∣ ( 𝑤 ⊆ 𝑥 ∧ Tr 𝑥 ) } ∈ V )
22 unexg ⊢ ( ( 𝑧 ∈ V ∧ ∪ 𝑤 ∈ 𝑧 ∩ { 𝑥 ∣ ( 𝑤 ⊆ 𝑥 ∧ Tr 𝑥 ) } ∈ V ) → ( 𝑧 ∪ ∪ 𝑤 ∈ 𝑧 ∩ { 𝑥 ∣ ( 𝑤 ⊆ 𝑥 ∧ Tr 𝑥 ) } ) ∈ V )
23 14 21 22 sylancr ⊢ ( ∀ 𝑤 ∈ 𝑧 ∃ 𝑥 ( 𝑤 ⊆ 𝑥 ∧ Tr 𝑥 ∧ ∀ 𝑦 ( ( 𝑤 ⊆ 𝑦 ∧ Tr 𝑦 ) → 𝑥 ⊆ 𝑦 ) ) → ( 𝑧 ∪ ∪ 𝑤 ∈ 𝑧 ∩ { 𝑥 ∣ ( 𝑤 ⊆ 𝑥 ∧ Tr 𝑥 ) } ) ∈ V )
24 ssun1 ⊢ 𝑧 ⊆ ( 𝑧 ∪ ∪ 𝑤 ∈ 𝑧 ∩ { 𝑥 ∣ ( 𝑤 ⊆ 𝑥 ∧ Tr 𝑥 ) } )
25 uniun ⊢ ∪ ( 𝑧 ∪ ∪ 𝑤 ∈ 𝑧 ∩ { 𝑥 ∣ ( 𝑤 ⊆ 𝑥 ∧ Tr 𝑥 ) } ) = ( ∪ 𝑧 ∪ ∪ ∪ 𝑤 ∈ 𝑧 ∩ { 𝑥 ∣ ( 𝑤 ⊆ 𝑥 ∧ Tr 𝑥 ) } )
26 uniiun ⊢ ∪ 𝑧 = ∪ 𝑤 ∈ 𝑧 𝑤
27 ssmin ⊢ 𝑤 ⊆ ∩ { 𝑥 ∣ ( 𝑤 ⊆ 𝑥 ∧ Tr 𝑥 ) }
28 27 rgenw ⊢ ∀ 𝑤 ∈ 𝑧 𝑤 ⊆ ∩ { 𝑥 ∣ ( 𝑤 ⊆ 𝑥 ∧ Tr 𝑥 ) }
29 ss2iun ⊢ ( ∀ 𝑤 ∈ 𝑧 𝑤 ⊆ ∩ { 𝑥 ∣ ( 𝑤 ⊆ 𝑥 ∧ Tr 𝑥 ) } → ∪ 𝑤 ∈ 𝑧 𝑤 ⊆ ∪ 𝑤 ∈ 𝑧 ∩ { 𝑥 ∣ ( 𝑤 ⊆ 𝑥 ∧ Tr 𝑥 ) } )
30 28 29 ax-mp ⊢ ∪ 𝑤 ∈ 𝑧 𝑤 ⊆ ∪ 𝑤 ∈ 𝑧 ∩ { 𝑥 ∣ ( 𝑤 ⊆ 𝑥 ∧ Tr 𝑥 ) }
31 26 30 eqsstri ⊢ ∪ 𝑧 ⊆ ∪ 𝑤 ∈ 𝑧 ∩ { 𝑥 ∣ ( 𝑤 ⊆ 𝑥 ∧ Tr 𝑥 ) }
32 ssun4 ⊢ ( ∪ 𝑧 ⊆ ∪ 𝑤 ∈ 𝑧 ∩ { 𝑥 ∣ ( 𝑤 ⊆ 𝑥 ∧ Tr 𝑥 ) } → ∪ 𝑧 ⊆ ( 𝑧 ∪ ∪ 𝑤 ∈ 𝑧 ∩ { 𝑥 ∣ ( 𝑤 ⊆ 𝑥 ∧ Tr 𝑥 ) } ) )
33 31 32 ax-mp ⊢ ∪ 𝑧 ⊆ ( 𝑧 ∪ ∪ 𝑤 ∈ 𝑧 ∩ { 𝑥 ∣ ( 𝑤 ⊆ 𝑥 ∧ Tr 𝑥 ) } )
34 trint ⊢ ( ∀ 𝑦 ∈ { 𝑥 ∣ ( 𝑤 ⊆ 𝑥 ∧ Tr 𝑥 ) } Tr 𝑦 → Tr ∩ { 𝑥 ∣ ( 𝑤 ⊆ 𝑥 ∧ Tr 𝑥 ) } )
35 sseq2 ⊢ ( 𝑥 = 𝑦 → ( 𝑤 ⊆ 𝑥 ↔ 𝑤 ⊆ 𝑦 ) )
36 treq ⊢ ( 𝑥 = 𝑦 → ( Tr 𝑥 ↔ Tr 𝑦 ) )
37 35 36 anbi12d ⊢ ( 𝑥 = 𝑦 → ( ( 𝑤 ⊆ 𝑥 ∧ Tr 𝑥 ) ↔ ( 𝑤 ⊆ 𝑦 ∧ Tr 𝑦 ) ) )
38 37 cbvabv ⊢ { 𝑥 ∣ ( 𝑤 ⊆ 𝑥 ∧ Tr 𝑥 ) } = { 𝑦 ∣ ( 𝑤 ⊆ 𝑦 ∧ Tr 𝑦 ) }
39 38 eqabri ⊢ ( 𝑦 ∈ { 𝑥 ∣ ( 𝑤 ⊆ 𝑥 ∧ Tr 𝑥 ) } ↔ ( 𝑤 ⊆ 𝑦 ∧ Tr 𝑦 ) )
40 39 simprbi ⊢ ( 𝑦 ∈ { 𝑥 ∣ ( 𝑤 ⊆ 𝑥 ∧ Tr 𝑥 ) } → Tr 𝑦 )
41 34 40 mprg ⊢ Tr ∩ { 𝑥 ∣ ( 𝑤 ⊆ 𝑥 ∧ Tr 𝑥 ) }
42 41 rgenw ⊢ ∀ 𝑤 ∈ 𝑧 Tr ∩ { 𝑥 ∣ ( 𝑤 ⊆ 𝑥 ∧ Tr 𝑥 ) }
43 triun ⊢ ( ∀ 𝑤 ∈ 𝑧 Tr ∩ { 𝑥 ∣ ( 𝑤 ⊆ 𝑥 ∧ Tr 𝑥 ) } → Tr ∪ 𝑤 ∈ 𝑧 ∩ { 𝑥 ∣ ( 𝑤 ⊆ 𝑥 ∧ Tr 𝑥 ) } )
44 42 43 ax-mp ⊢ Tr ∪ 𝑤 ∈ 𝑧 ∩ { 𝑥 ∣ ( 𝑤 ⊆ 𝑥 ∧ Tr 𝑥 ) }
45 df-tr ⊢ ( Tr ∪ 𝑤 ∈ 𝑧 ∩ { 𝑥 ∣ ( 𝑤 ⊆ 𝑥 ∧ Tr 𝑥 ) } ↔ ∪ ∪ 𝑤 ∈ 𝑧 ∩ { 𝑥 ∣ ( 𝑤 ⊆ 𝑥 ∧ Tr 𝑥 ) } ⊆ ∪ 𝑤 ∈ 𝑧 ∩ { 𝑥 ∣ ( 𝑤 ⊆ 𝑥 ∧ Tr 𝑥 ) } )
46 44 45 mpbi ⊢ ∪ ∪ 𝑤 ∈ 𝑧 ∩ { 𝑥 ∣ ( 𝑤 ⊆ 𝑥 ∧ Tr 𝑥 ) } ⊆ ∪ 𝑤 ∈ 𝑧 ∩ { 𝑥 ∣ ( 𝑤 ⊆ 𝑥 ∧ Tr 𝑥 ) }
47 ssun4 ⊢ ( ∪ ∪ 𝑤 ∈ 𝑧 ∩ { 𝑥 ∣ ( 𝑤 ⊆ 𝑥 ∧ Tr 𝑥 ) } ⊆ ∪ 𝑤 ∈ 𝑧 ∩ { 𝑥 ∣ ( 𝑤 ⊆ 𝑥 ∧ Tr 𝑥 ) } → ∪ ∪ 𝑤 ∈ 𝑧 ∩ { 𝑥 ∣ ( 𝑤 ⊆ 𝑥 ∧ Tr 𝑥 ) } ⊆ ( 𝑧 ∪ ∪ 𝑤 ∈ 𝑧 ∩ { 𝑥 ∣ ( 𝑤 ⊆ 𝑥 ∧ Tr 𝑥 ) } ) )
48 46 47 ax-mp ⊢ ∪ ∪ 𝑤 ∈ 𝑧 ∩ { 𝑥 ∣ ( 𝑤 ⊆ 𝑥 ∧ Tr 𝑥 ) } ⊆ ( 𝑧 ∪ ∪ 𝑤 ∈ 𝑧 ∩ { 𝑥 ∣ ( 𝑤 ⊆ 𝑥 ∧ Tr 𝑥 ) } )
49 33 48 unssi ⊢ ( ∪ 𝑧 ∪ ∪ ∪ 𝑤 ∈ 𝑧 ∩ { 𝑥 ∣ ( 𝑤 ⊆ 𝑥 ∧ Tr 𝑥 ) } ) ⊆ ( 𝑧 ∪ ∪ 𝑤 ∈ 𝑧 ∩ { 𝑥 ∣ ( 𝑤 ⊆ 𝑥 ∧ Tr 𝑥 ) } )
50 25 49 eqsstri ⊢ ∪ ( 𝑧 ∪ ∪ 𝑤 ∈ 𝑧 ∩ { 𝑥 ∣ ( 𝑤 ⊆ 𝑥 ∧ Tr 𝑥 ) } ) ⊆ ( 𝑧 ∪ ∪ 𝑤 ∈ 𝑧 ∩ { 𝑥 ∣ ( 𝑤 ⊆ 𝑥 ∧ Tr 𝑥 ) } )
51 df-tr ⊢ ( Tr ( 𝑧 ∪ ∪ 𝑤 ∈ 𝑧 ∩ { 𝑥 ∣ ( 𝑤 ⊆ 𝑥 ∧ Tr 𝑥 ) } ) ↔ ∪ ( 𝑧 ∪ ∪ 𝑤 ∈ 𝑧 ∩ { 𝑥 ∣ ( 𝑤 ⊆ 𝑥 ∧ Tr 𝑥 ) } ) ⊆ ( 𝑧 ∪ ∪ 𝑤 ∈ 𝑧 ∩ { 𝑥 ∣ ( 𝑤 ⊆ 𝑥 ∧ Tr 𝑥 ) } ) )
52 50 51 mpbir ⊢ Tr ( 𝑧 ∪ ∪ 𝑤 ∈ 𝑧 ∩ { 𝑥 ∣ ( 𝑤 ⊆ 𝑥 ∧ Tr 𝑥 ) } )
53 ssel ⊢ ( 𝑧 ⊆ 𝑦 → ( 𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑦 ) )
54 trss ⊢ ( Tr 𝑦 → ( 𝑤 ∈ 𝑦 → 𝑤 ⊆ 𝑦 ) )
55 53 54 sylan9 ⊢ ( ( 𝑧 ⊆ 𝑦 ∧ Tr 𝑦 ) → ( 𝑤 ∈ 𝑧 → 𝑤 ⊆ 𝑦 ) )
56 simpr ⊢ ( ( 𝑧 ⊆ 𝑦 ∧ Tr 𝑦 ) → Tr 𝑦 )
57 55 56 jctird ⊢ ( ( 𝑧 ⊆ 𝑦 ∧ Tr 𝑦 ) → ( 𝑤 ∈ 𝑧 → ( 𝑤 ⊆ 𝑦 ∧ Tr 𝑦 ) ) )
58 rabab ⊢ { 𝑥 ∈ V ∣ ( 𝑤 ⊆ 𝑥 ∧ Tr 𝑥 ) } = { 𝑥 ∣ ( 𝑤 ⊆ 𝑥 ∧ Tr 𝑥 ) }
59 58 inteqi ⊢ ∩ { 𝑥 ∈ V ∣ ( 𝑤 ⊆ 𝑥 ∧ Tr 𝑥 ) } = ∩ { 𝑥 ∣ ( 𝑤 ⊆ 𝑥 ∧ Tr 𝑥 ) }
60 vex ⊢ 𝑦 ∈ V
61 37 intminss ⊢ ( ( 𝑦 ∈ V ∧ ( 𝑤 ⊆ 𝑦 ∧ Tr 𝑦 ) ) → ∩ { 𝑥 ∈ V ∣ ( 𝑤 ⊆ 𝑥 ∧ Tr 𝑥 ) } ⊆ 𝑦 )
62 60 61 mpan ⊢ ( ( 𝑤 ⊆ 𝑦 ∧ Tr 𝑦 ) → ∩ { 𝑥 ∈ V ∣ ( 𝑤 ⊆ 𝑥 ∧ Tr 𝑥 ) } ⊆ 𝑦 )
63 59 62 eqsstrrid ⊢ ( ( 𝑤 ⊆ 𝑦 ∧ Tr 𝑦 ) → ∩ { 𝑥 ∣ ( 𝑤 ⊆ 𝑥 ∧ Tr 𝑥 ) } ⊆ 𝑦 )
64 57 63 syl6 ⊢ ( ( 𝑧 ⊆ 𝑦 ∧ Tr 𝑦 ) → ( 𝑤 ∈ 𝑧 → ∩ { 𝑥 ∣ ( 𝑤 ⊆ 𝑥 ∧ Tr 𝑥 ) } ⊆ 𝑦 ) )
65 64 ralrimiv ⊢ ( ( 𝑧 ⊆ 𝑦 ∧ Tr 𝑦 ) → ∀ 𝑤 ∈ 𝑧 ∩ { 𝑥 ∣ ( 𝑤 ⊆ 𝑥 ∧ Tr 𝑥 ) } ⊆ 𝑦 )
66 iunss ⊢ ( ∪ 𝑤 ∈ 𝑧 ∩ { 𝑥 ∣ ( 𝑤 ⊆ 𝑥 ∧ Tr 𝑥 ) } ⊆ 𝑦 ↔ ∀ 𝑤 ∈ 𝑧 ∩ { 𝑥 ∣ ( 𝑤 ⊆ 𝑥 ∧ Tr 𝑥 ) } ⊆ 𝑦 )
67 65 66 sylibr ⊢ ( ( 𝑧 ⊆ 𝑦 ∧ Tr 𝑦 ) → ∪ 𝑤 ∈ 𝑧 ∩ { 𝑥 ∣ ( 𝑤 ⊆ 𝑥 ∧ Tr 𝑥 ) } ⊆ 𝑦 )
68 unss ⊢ ( ( 𝑧 ⊆ 𝑦 ∧ ∪ 𝑤 ∈ 𝑧 ∩ { 𝑥 ∣ ( 𝑤 ⊆ 𝑥 ∧ Tr 𝑥 ) } ⊆ 𝑦 ) ↔ ( 𝑧 ∪ ∪ 𝑤 ∈ 𝑧 ∩ { 𝑥 ∣ ( 𝑤 ⊆ 𝑥 ∧ Tr 𝑥 ) } ) ⊆ 𝑦 )
69 68 biimpi ⊢ ( ( 𝑧 ⊆ 𝑦 ∧ ∪ 𝑤 ∈ 𝑧 ∩ { 𝑥 ∣ ( 𝑤 ⊆ 𝑥 ∧ Tr 𝑥 ) } ⊆ 𝑦 ) → ( 𝑧 ∪ ∪ 𝑤 ∈ 𝑧 ∩ { 𝑥 ∣ ( 𝑤 ⊆ 𝑥 ∧ Tr 𝑥 ) } ) ⊆ 𝑦 )
70 67 69 syldan ⊢ ( ( 𝑧 ⊆ 𝑦 ∧ Tr 𝑦 ) → ( 𝑧 ∪ ∪ 𝑤 ∈ 𝑧 ∩ { 𝑥 ∣ ( 𝑤 ⊆ 𝑥 ∧ Tr 𝑥 ) } ) ⊆ 𝑦 )
71 70 ax-gen ⊢ ∀ 𝑦 ( ( 𝑧 ⊆ 𝑦 ∧ Tr 𝑦 ) → ( 𝑧 ∪ ∪ 𝑤 ∈ 𝑧 ∩ { 𝑥 ∣ ( 𝑤 ⊆ 𝑥 ∧ Tr 𝑥 ) } ) ⊆ 𝑦 )
72 24 52 71 3pm3.2i ⊢ ( 𝑧 ⊆ ( 𝑧 ∪ ∪ 𝑤 ∈ 𝑧 ∩ { 𝑥 ∣ ( 𝑤 ⊆ 𝑥 ∧ Tr 𝑥 ) } ) ∧ Tr ( 𝑧 ∪ ∪ 𝑤 ∈ 𝑧 ∩ { 𝑥 ∣ ( 𝑤 ⊆ 𝑥 ∧ Tr 𝑥 ) } ) ∧ ∀ 𝑦 ( ( 𝑧 ⊆ 𝑦 ∧ Tr 𝑦 ) → ( 𝑧 ∪ ∪ 𝑤 ∈ 𝑧 ∩ { 𝑥 ∣ ( 𝑤 ⊆ 𝑥 ∧ Tr 𝑥 ) } ) ⊆ 𝑦 ) )
73 sseq2 ⊢ ( 𝑢 = ( 𝑧 ∪ ∪ 𝑤 ∈ 𝑧 ∩ { 𝑥 ∣ ( 𝑤 ⊆ 𝑥 ∧ Tr 𝑥 ) } ) → ( 𝑧 ⊆ 𝑢 ↔ 𝑧 ⊆ ( 𝑧 ∪ ∪ 𝑤 ∈ 𝑧 ∩ { 𝑥 ∣ ( 𝑤 ⊆ 𝑥 ∧ Tr 𝑥 ) } ) ) )
74 treq ⊢ ( 𝑢 = ( 𝑧 ∪ ∪ 𝑤 ∈ 𝑧 ∩ { 𝑥 ∣ ( 𝑤 ⊆ 𝑥 ∧ Tr 𝑥 ) } ) → ( Tr 𝑢 ↔ Tr ( 𝑧 ∪ ∪ 𝑤 ∈ 𝑧 ∩ { 𝑥 ∣ ( 𝑤 ⊆ 𝑥 ∧ Tr 𝑥 ) } ) ) )
75 sseq1 ⊢ ( 𝑢 = ( 𝑧 ∪ ∪ 𝑤 ∈ 𝑧 ∩ { 𝑥 ∣ ( 𝑤 ⊆ 𝑥 ∧ Tr 𝑥 ) } ) → ( 𝑢 ⊆ 𝑦 ↔ ( 𝑧 ∪ ∪ 𝑤 ∈ 𝑧 ∩ { 𝑥 ∣ ( 𝑤 ⊆ 𝑥 ∧ Tr 𝑥 ) } ) ⊆ 𝑦 ) )
76 75 imbi2d ⊢ ( 𝑢 = ( 𝑧 ∪ ∪ 𝑤 ∈ 𝑧 ∩ { 𝑥 ∣ ( 𝑤 ⊆ 𝑥 ∧ Tr 𝑥 ) } ) → ( ( ( 𝑧 ⊆ 𝑦 ∧ Tr 𝑦 ) → 𝑢 ⊆ 𝑦 ) ↔ ( ( 𝑧 ⊆ 𝑦 ∧ Tr 𝑦 ) → ( 𝑧 ∪ ∪ 𝑤 ∈ 𝑧 ∩ { 𝑥 ∣ ( 𝑤 ⊆ 𝑥 ∧ Tr 𝑥 ) } ) ⊆ 𝑦 ) ) )
77 76 albidv ⊢ ( 𝑢 = ( 𝑧 ∪ ∪ 𝑤 ∈ 𝑧 ∩ { 𝑥 ∣ ( 𝑤 ⊆ 𝑥 ∧ Tr 𝑥 ) } ) → ( ∀ 𝑦 ( ( 𝑧 ⊆ 𝑦 ∧ Tr 𝑦 ) → 𝑢 ⊆ 𝑦 ) ↔ ∀ 𝑦 ( ( 𝑧 ⊆ 𝑦 ∧ Tr 𝑦 ) → ( 𝑧 ∪ ∪ 𝑤 ∈ 𝑧 ∩ { 𝑥 ∣ ( 𝑤 ⊆ 𝑥 ∧ Tr 𝑥 ) } ) ⊆ 𝑦 ) ) )
78 73 74 77 3anbi123d ⊢ ( 𝑢 = ( 𝑧 ∪ ∪ 𝑤 ∈ 𝑧 ∩ { 𝑥 ∣ ( 𝑤 ⊆ 𝑥 ∧ Tr 𝑥 ) } ) → ( ( 𝑧 ⊆ 𝑢 ∧ Tr 𝑢 ∧ ∀ 𝑦 ( ( 𝑧 ⊆ 𝑦 ∧ Tr 𝑦 ) → 𝑢 ⊆ 𝑦 ) ) ↔ ( 𝑧 ⊆ ( 𝑧 ∪ ∪ 𝑤 ∈ 𝑧 ∩ { 𝑥 ∣ ( 𝑤 ⊆ 𝑥 ∧ Tr 𝑥 ) } ) ∧ Tr ( 𝑧 ∪ ∪ 𝑤 ∈ 𝑧 ∩ { 𝑥 ∣ ( 𝑤 ⊆ 𝑥 ∧ Tr 𝑥 ) } ) ∧ ∀ 𝑦 ( ( 𝑧 ⊆ 𝑦 ∧ Tr 𝑦 ) → ( 𝑧 ∪ ∪ 𝑤 ∈ 𝑧 ∩ { 𝑥 ∣ ( 𝑤 ⊆ 𝑥 ∧ Tr 𝑥 ) } ) ⊆ 𝑦 ) ) ) )
79 78 spcegv ⊢ ( ( 𝑧 ∪ ∪ 𝑤 ∈ 𝑧 ∩ { 𝑥 ∣ ( 𝑤 ⊆ 𝑥 ∧ Tr 𝑥 ) } ) ∈ V → ( ( 𝑧 ⊆ ( 𝑧 ∪ ∪ 𝑤 ∈ 𝑧 ∩ { 𝑥 ∣ ( 𝑤 ⊆ 𝑥 ∧ Tr 𝑥 ) } ) ∧ Tr ( 𝑧 ∪ ∪ 𝑤 ∈ 𝑧 ∩ { 𝑥 ∣ ( 𝑤 ⊆ 𝑥 ∧ Tr 𝑥 ) } ) ∧ ∀ 𝑦 ( ( 𝑧 ⊆ 𝑦 ∧ Tr 𝑦 ) → ( 𝑧 ∪ ∪ 𝑤 ∈ 𝑧 ∩ { 𝑥 ∣ ( 𝑤 ⊆ 𝑥 ∧ Tr 𝑥 ) } ) ⊆ 𝑦 ) ) → ∃ 𝑢 ( 𝑧 ⊆ 𝑢 ∧ Tr 𝑢 ∧ ∀ 𝑦 ( ( 𝑧 ⊆ 𝑦 ∧ Tr 𝑦 ) → 𝑢 ⊆ 𝑦 ) ) ) )
80 sseq2 ⊢ ( 𝑢 = 𝑥 → ( 𝑧 ⊆ 𝑢 ↔ 𝑧 ⊆ 𝑥 ) )
81 treq ⊢ ( 𝑢 = 𝑥 → ( Tr 𝑢 ↔ Tr 𝑥 ) )
82 sseq1 ⊢ ( 𝑢 = 𝑥 → ( 𝑢 ⊆ 𝑦 ↔ 𝑥 ⊆ 𝑦 ) )
83 82 imbi2d ⊢ ( 𝑢 = 𝑥 → ( ( ( 𝑧 ⊆ 𝑦 ∧ Tr 𝑦 ) → 𝑢 ⊆ 𝑦 ) ↔ ( ( 𝑧 ⊆ 𝑦 ∧ Tr 𝑦 ) → 𝑥 ⊆ 𝑦 ) ) )
84 83 albidv ⊢ ( 𝑢 = 𝑥 → ( ∀ 𝑦 ( ( 𝑧 ⊆ 𝑦 ∧ Tr 𝑦 ) → 𝑢 ⊆ 𝑦 ) ↔ ∀ 𝑦 ( ( 𝑧 ⊆ 𝑦 ∧ Tr 𝑦 ) → 𝑥 ⊆ 𝑦 ) ) )
85 80 81 84 3anbi123d ⊢ ( 𝑢 = 𝑥 → ( ( 𝑧 ⊆ 𝑢 ∧ Tr 𝑢 ∧ ∀ 𝑦 ( ( 𝑧 ⊆ 𝑦 ∧ Tr 𝑦 ) → 𝑢 ⊆ 𝑦 ) ) ↔ ( 𝑧 ⊆ 𝑥 ∧ Tr 𝑥 ∧ ∀ 𝑦 ( ( 𝑧 ⊆ 𝑦 ∧ Tr 𝑦 ) → 𝑥 ⊆ 𝑦 ) ) ) )
86 85 cbvexvw ⊢ ( ∃ 𝑢 ( 𝑧 ⊆ 𝑢 ∧ Tr 𝑢 ∧ ∀ 𝑦 ( ( 𝑧 ⊆ 𝑦 ∧ Tr 𝑦 ) → 𝑢 ⊆ 𝑦 ) ) ↔ ∃ 𝑥 ( 𝑧 ⊆ 𝑥 ∧ Tr 𝑥 ∧ ∀ 𝑦 ( ( 𝑧 ⊆ 𝑦 ∧ Tr 𝑦 ) → 𝑥 ⊆ 𝑦 ) ) )
87 79 86 imbitrdi ⊢ ( ( 𝑧 ∪ ∪ 𝑤 ∈ 𝑧 ∩ { 𝑥 ∣ ( 𝑤 ⊆ 𝑥 ∧ Tr 𝑥 ) } ) ∈ V → ( ( 𝑧 ⊆ ( 𝑧 ∪ ∪ 𝑤 ∈ 𝑧 ∩ { 𝑥 ∣ ( 𝑤 ⊆ 𝑥 ∧ Tr 𝑥 ) } ) ∧ Tr ( 𝑧 ∪ ∪ 𝑤 ∈ 𝑧 ∩ { 𝑥 ∣ ( 𝑤 ⊆ 𝑥 ∧ Tr 𝑥 ) } ) ∧ ∀ 𝑦 ( ( 𝑧 ⊆ 𝑦 ∧ Tr 𝑦 ) → ( 𝑧 ∪ ∪ 𝑤 ∈ 𝑧 ∩ { 𝑥 ∣ ( 𝑤 ⊆ 𝑥 ∧ Tr 𝑥 ) } ) ⊆ 𝑦 ) ) → ∃ 𝑥 ( 𝑧 ⊆ 𝑥 ∧ Tr 𝑥 ∧ ∀ 𝑦 ( ( 𝑧 ⊆ 𝑦 ∧ Tr 𝑦 ) → 𝑥 ⊆ 𝑦 ) ) ) )
88 23 72 87 mpisyl ⊢ ( ∀ 𝑤 ∈ 𝑧 ∃ 𝑥 ( 𝑤 ⊆ 𝑥 ∧ Tr 𝑥 ∧ ∀ 𝑦 ( ( 𝑤 ⊆ 𝑦 ∧ Tr 𝑦 ) → 𝑥 ⊆ 𝑦 ) ) → ∃ 𝑥 ( 𝑧 ⊆ 𝑥 ∧ Tr 𝑥 ∧ ∀ 𝑦 ( ( 𝑧 ⊆ 𝑦 ∧ Tr 𝑦 ) → 𝑥 ⊆ 𝑦 ) ) )
89 13 88 setinds2regs ⊢ ∃ 𝑥 ( 𝑧 ⊆ 𝑥 ∧ Tr 𝑥 ∧ ∀ 𝑦 ( ( 𝑧 ⊆ 𝑦 ∧ Tr 𝑦 ) → 𝑥 ⊆ 𝑦 ) )
90 1 7 89 vtocl ⊢ ∃ 𝑥 ( 𝐴 ⊆ 𝑥 ∧ Tr 𝑥 ∧ ∀ 𝑦 ( ( 𝐴 ⊆ 𝑦 ∧ Tr 𝑦 ) → 𝑥 ⊆ 𝑦 ) )