Metamath Proof Explorer

Theorem dfon2lem3

Description: Lemma for dfon2 . All sets satisfying the new definition are transitive and untangled. (Contributed by Scott Fenton, 25-Feb-2011)

Ref Expression
Assertion dfon2lem3 ( 𝐴 ∈ 𝑉 → ( ∀ 𝑥 ( ( 𝑥 ⊊ 𝐴 ∧ Tr 𝑥 ) → 𝑥 ∈ 𝐴 ) → ( Tr 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ¬ 𝑧 ∈ 𝑧 ) ) )

Proof

Step Hyp Ref Expression
1 untelirr ⊢ ( ∀ 𝑧 ∈ ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ¬ 𝑡 ∈ 𝑡 ) } ¬ 𝑧 ∈ 𝑧 → ¬ ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ¬ 𝑡 ∈ 𝑡 ) } ∈ ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ¬ 𝑡 ∈ 𝑡 ) } )
2 eluni2 ⊢ ( 𝑧 ∈ ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ¬ 𝑡 ∈ 𝑡 ) } ↔ ∃ 𝑥 ∈ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ¬ 𝑡 ∈ 𝑡 ) } 𝑧 ∈ 𝑥 )
3 vex ⊢ 𝑥 ∈ V
4 sseq1 ⊢ ( 𝑤 = 𝑥 → ( 𝑤 ⊆ 𝐴 ↔ 𝑥 ⊆ 𝐴 ) )
5 treq ⊢ ( 𝑤 = 𝑥 → ( Tr 𝑤 ↔ Tr 𝑥 ) )
6 raleq ⊢ ( 𝑤 = 𝑥 → ( ∀ 𝑡 ∈ 𝑤 ¬ 𝑡 ∈ 𝑡 ↔ ∀ 𝑡 ∈ 𝑥 ¬ 𝑡 ∈ 𝑡 ) )
7 4 5 6 3anbi123d ⊢ ( 𝑤 = 𝑥 → ( ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ¬ 𝑡 ∈ 𝑡 ) ↔ ( 𝑥 ⊆ 𝐴 ∧ Tr 𝑥 ∧ ∀ 𝑡 ∈ 𝑥 ¬ 𝑡 ∈ 𝑡 ) ) )
8 3 7 elab ⊢ ( 𝑥 ∈ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ¬ 𝑡 ∈ 𝑡 ) } ↔ ( 𝑥 ⊆ 𝐴 ∧ Tr 𝑥 ∧ ∀ 𝑡 ∈ 𝑥 ¬ 𝑡 ∈ 𝑡 ) )
9 elequ1 ⊢ ( 𝑡 = 𝑧 → ( 𝑡 ∈ 𝑡 ↔ 𝑧 ∈ 𝑡 ) )
10 elequ2 ⊢ ( 𝑡 = 𝑧 → ( 𝑧 ∈ 𝑡 ↔ 𝑧 ∈ 𝑧 ) )
11 9 10 bitrd ⊢ ( 𝑡 = 𝑧 → ( 𝑡 ∈ 𝑡 ↔ 𝑧 ∈ 𝑧 ) )
12 11 notbid ⊢ ( 𝑡 = 𝑧 → ( ¬ 𝑡 ∈ 𝑡 ↔ ¬ 𝑧 ∈ 𝑧 ) )
13 12 cbvralvw ⊢ ( ∀ 𝑡 ∈ 𝑥 ¬ 𝑡 ∈ 𝑡 ↔ ∀ 𝑧 ∈ 𝑥 ¬ 𝑧 ∈ 𝑧 )
14 13 biimpi ⊢ ( ∀ 𝑡 ∈ 𝑥 ¬ 𝑡 ∈ 𝑡 → ∀ 𝑧 ∈ 𝑥 ¬ 𝑧 ∈ 𝑧 )
15 14 3ad2ant3 ⊢ ( ( 𝑥 ⊆ 𝐴 ∧ Tr 𝑥 ∧ ∀ 𝑡 ∈ 𝑥 ¬ 𝑡 ∈ 𝑡 ) → ∀ 𝑧 ∈ 𝑥 ¬ 𝑧 ∈ 𝑧 )
16 8 15 sylbi ⊢ ( 𝑥 ∈ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ¬ 𝑡 ∈ 𝑡 ) } → ∀ 𝑧 ∈ 𝑥 ¬ 𝑧 ∈ 𝑧 )
17 rsp ⊢ ( ∀ 𝑧 ∈ 𝑥 ¬ 𝑧 ∈ 𝑧 → ( 𝑧 ∈ 𝑥 → ¬ 𝑧 ∈ 𝑧 ) )
18 16 17 syl ⊢ ( 𝑥 ∈ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ¬ 𝑡 ∈ 𝑡 ) } → ( 𝑧 ∈ 𝑥 → ¬ 𝑧 ∈ 𝑧 ) )
19 18 rexlimiv ⊢ ( ∃ 𝑥 ∈ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ¬ 𝑡 ∈ 𝑡 ) } 𝑧 ∈ 𝑥 → ¬ 𝑧 ∈ 𝑧 )
20 2 19 sylbi ⊢ ( 𝑧 ∈ ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ¬ 𝑡 ∈ 𝑡 ) } → ¬ 𝑧 ∈ 𝑧 )
21 1 20 mprg ⊢ ¬ ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ¬ 𝑡 ∈ 𝑡 ) } ∈ ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ¬ 𝑡 ∈ 𝑡 ) }
22 dfon2lem2 ⊢ ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ¬ 𝑡 ∈ 𝑡 ) } ⊆ 𝐴
23 dfpss2 ⊢ ( ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ¬ 𝑡 ∈ 𝑡 ) } ⊊ 𝐴 ↔ ( ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ¬ 𝑡 ∈ 𝑡 ) } ⊆ 𝐴 ∧ ¬ ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ¬ 𝑡 ∈ 𝑡 ) } = 𝐴 ) )
24 dfon2lem1 ⊢ Tr ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ¬ 𝑡 ∈ 𝑡 ) }
25 ssexg ⊢ ( ( ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ¬ 𝑡 ∈ 𝑡 ) } ⊆ 𝐴 ∧ 𝐴 ∈ 𝑉 ) → ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ¬ 𝑡 ∈ 𝑡 ) } ∈ V )
26 22 25 mpan ⊢ ( 𝐴 ∈ 𝑉 → ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ¬ 𝑡 ∈ 𝑡 ) } ∈ V )
27 psseq1 ⊢ ( 𝑥 = ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ¬ 𝑡 ∈ 𝑡 ) } → ( 𝑥 ⊊ 𝐴 ↔ ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ¬ 𝑡 ∈ 𝑡 ) } ⊊ 𝐴 ) )
28 treq ⊢ ( 𝑥 = ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ¬ 𝑡 ∈ 𝑡 ) } → ( Tr 𝑥 ↔ Tr ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ¬ 𝑡 ∈ 𝑡 ) } ) )
29 27 28 anbi12d ⊢ ( 𝑥 = ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ¬ 𝑡 ∈ 𝑡 ) } → ( ( 𝑥 ⊊ 𝐴 ∧ Tr 𝑥 ) ↔ ( ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ¬ 𝑡 ∈ 𝑡 ) } ⊊ 𝐴 ∧ Tr ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ¬ 𝑡 ∈ 𝑡 ) } ) ) )
30 eleq1 ⊢ ( 𝑥 = ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ¬ 𝑡 ∈ 𝑡 ) } → ( 𝑥 ∈ 𝐴 ↔ ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ¬ 𝑡 ∈ 𝑡 ) } ∈ 𝐴 ) )
31 29 30 imbi12d ⊢ ( 𝑥 = ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ¬ 𝑡 ∈ 𝑡 ) } → ( ( ( 𝑥 ⊊ 𝐴 ∧ Tr 𝑥 ) → 𝑥 ∈ 𝐴 ) ↔ ( ( ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ¬ 𝑡 ∈ 𝑡 ) } ⊊ 𝐴 ∧ Tr ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ¬ 𝑡 ∈ 𝑡 ) } ) → ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ¬ 𝑡 ∈ 𝑡 ) } ∈ 𝐴 ) ) )
32 31 spcgv ⊢ ( ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ¬ 𝑡 ∈ 𝑡 ) } ∈ V → ( ∀ 𝑥 ( ( 𝑥 ⊊ 𝐴 ∧ Tr 𝑥 ) → 𝑥 ∈ 𝐴 ) → ( ( ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ¬ 𝑡 ∈ 𝑡 ) } ⊊ 𝐴 ∧ Tr ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ¬ 𝑡 ∈ 𝑡 ) } ) → ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ¬ 𝑡 ∈ 𝑡 ) } ∈ 𝐴 ) ) )
33 32 imp ⊢ ( ( ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ¬ 𝑡 ∈ 𝑡 ) } ∈ V ∧ ∀ 𝑥 ( ( 𝑥 ⊊ 𝐴 ∧ Tr 𝑥 ) → 𝑥 ∈ 𝐴 ) ) → ( ( ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ¬ 𝑡 ∈ 𝑡 ) } ⊊ 𝐴 ∧ Tr ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ¬ 𝑡 ∈ 𝑡 ) } ) → ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ¬ 𝑡 ∈ 𝑡 ) } ∈ 𝐴 ) )
34 26 33 sylan ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ∀ 𝑥 ( ( 𝑥 ⊊ 𝐴 ∧ Tr 𝑥 ) → 𝑥 ∈ 𝐴 ) ) → ( ( ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ¬ 𝑡 ∈ 𝑡 ) } ⊊ 𝐴 ∧ Tr ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ¬ 𝑡 ∈ 𝑡 ) } ) → ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ¬ 𝑡 ∈ 𝑡 ) } ∈ 𝐴 ) )
35 snssi ⊢ ( ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ¬ 𝑡 ∈ 𝑡 ) } ∈ 𝐴 → { ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ¬ 𝑡 ∈ 𝑡 ) } } ⊆ 𝐴 )
36 unss ⊢ ( ( ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ¬ 𝑡 ∈ 𝑡 ) } ⊆ 𝐴 ∧ { ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ¬ 𝑡 ∈ 𝑡 ) } } ⊆ 𝐴 ) ↔ ( ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ¬ 𝑡 ∈ 𝑡 ) } ∪ { ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ¬ 𝑡 ∈ 𝑡 ) } } ) ⊆ 𝐴 )
37 df-suc ⊢ suc ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ¬ 𝑡 ∈ 𝑡 ) } = ( ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ¬ 𝑡 ∈ 𝑡 ) } ∪ { ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ¬ 𝑡 ∈ 𝑡 ) } } )
38 37 sseq1i ⊢ ( suc ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ¬ 𝑡 ∈ 𝑡 ) } ⊆ 𝐴 ↔ ( ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ¬ 𝑡 ∈ 𝑡 ) } ∪ { ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ¬ 𝑡 ∈ 𝑡 ) } } ) ⊆ 𝐴 )
39 36 38 sylbb2 ⊢ ( ( ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ¬ 𝑡 ∈ 𝑡 ) } ⊆ 𝐴 ∧ { ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ¬ 𝑡 ∈ 𝑡 ) } } ⊆ 𝐴 ) → suc ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ¬ 𝑡 ∈ 𝑡 ) } ⊆ 𝐴 )
40 22 35 39 sylancr ⊢ ( ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ¬ 𝑡 ∈ 𝑡 ) } ∈ 𝐴 → suc ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ¬ 𝑡 ∈ 𝑡 ) } ⊆ 𝐴 )
41 suctr ⊢ ( Tr ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ¬ 𝑡 ∈ 𝑡 ) } → Tr suc ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ¬ 𝑡 ∈ 𝑡 ) } )
42 24 41 ax-mp ⊢ Tr suc ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ¬ 𝑡 ∈ 𝑡 ) }
43 untuni ⊢ ( ∀ 𝑧 ∈ ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ¬ 𝑡 ∈ 𝑡 ) } ¬ 𝑧 ∈ 𝑧 ↔ ∀ 𝑥 ∈ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ¬ 𝑡 ∈ 𝑡 ) } ∀ 𝑧 ∈ 𝑥 ¬ 𝑧 ∈ 𝑧 )
44 43 16 mprgbir ⊢ ∀ 𝑧 ∈ ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ¬ 𝑡 ∈ 𝑡 ) } ¬ 𝑧 ∈ 𝑧
45 nfv ⊢ Ⅎ 𝑡 𝑤 ⊆ 𝐴
46 nfv ⊢ Ⅎ 𝑡 Tr 𝑤
47 nfra1 ⊢ Ⅎ 𝑡 ∀ 𝑡 ∈ 𝑤 ¬ 𝑡 ∈ 𝑡
48 45 46 47 nf3an ⊢ Ⅎ 𝑡 ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ¬ 𝑡 ∈ 𝑡 )
49 48 nfab ⊢ Ⅎ 𝑡 { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ¬ 𝑡 ∈ 𝑡 ) }
50 49 nfuni ⊢ Ⅎ 𝑡 ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ¬ 𝑡 ∈ 𝑡 ) }
51 50 untsucf ⊢ ( ∀ 𝑧 ∈ ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ¬ 𝑡 ∈ 𝑡 ) } ¬ 𝑧 ∈ 𝑧 → ∀ 𝑡 ∈ suc ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ¬ 𝑡 ∈ 𝑡 ) } ¬ 𝑡 ∈ 𝑡 )
52 44 51 ax-mp ⊢ ∀ 𝑡 ∈ suc ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ¬ 𝑡 ∈ 𝑡 ) } ¬ 𝑡 ∈ 𝑡
53 sseq1 ⊢ ( 𝑧 = suc ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ¬ 𝑡 ∈ 𝑡 ) } → ( 𝑧 ⊆ 𝐴 ↔ suc ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ¬ 𝑡 ∈ 𝑡 ) } ⊆ 𝐴 ) )
54 treq ⊢ ( 𝑧 = suc ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ¬ 𝑡 ∈ 𝑡 ) } → ( Tr 𝑧 ↔ Tr suc ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ¬ 𝑡 ∈ 𝑡 ) } ) )
55 nfcv ⊢ Ⅎ 𝑡 𝑧
56 50 nfsuc ⊢ Ⅎ 𝑡 suc ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ¬ 𝑡 ∈ 𝑡 ) }
57 55 56 raleqf ⊢ ( 𝑧 = suc ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ¬ 𝑡 ∈ 𝑡 ) } → ( ∀ 𝑡 ∈ 𝑧 ¬ 𝑡 ∈ 𝑡 ↔ ∀ 𝑡 ∈ suc ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ¬ 𝑡 ∈ 𝑡 ) } ¬ 𝑡 ∈ 𝑡 ) )
58 53 54 57 3anbi123d ⊢ ( 𝑧 = suc ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ¬ 𝑡 ∈ 𝑡 ) } → ( ( 𝑧 ⊆ 𝐴 ∧ Tr 𝑧 ∧ ∀ 𝑡 ∈ 𝑧 ¬ 𝑡 ∈ 𝑡 ) ↔ ( suc ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ¬ 𝑡 ∈ 𝑡 ) } ⊆ 𝐴 ∧ Tr suc ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ¬ 𝑡 ∈ 𝑡 ) } ∧ ∀ 𝑡 ∈ suc ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ¬ 𝑡 ∈ 𝑡 ) } ¬ 𝑡 ∈ 𝑡 ) ) )
59 sseq1 ⊢ ( 𝑤 = 𝑧 → ( 𝑤 ⊆ 𝐴 ↔ 𝑧 ⊆ 𝐴 ) )
60 treq ⊢ ( 𝑤 = 𝑧 → ( Tr 𝑤 ↔ Tr 𝑧 ) )
61 raleq ⊢ ( 𝑤 = 𝑧 → ( ∀ 𝑡 ∈ 𝑤 ¬ 𝑡 ∈ 𝑡 ↔ ∀ 𝑡 ∈ 𝑧 ¬ 𝑡 ∈ 𝑡 ) )
62 59 60 61 3anbi123d ⊢ ( 𝑤 = 𝑧 → ( ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ¬ 𝑡 ∈ 𝑡 ) ↔ ( 𝑧 ⊆ 𝐴 ∧ Tr 𝑧 ∧ ∀ 𝑡 ∈ 𝑧 ¬ 𝑡 ∈ 𝑡 ) ) )
63 62 cbvabv ⊢ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ¬ 𝑡 ∈ 𝑡 ) } = { 𝑧 ∣ ( 𝑧 ⊆ 𝐴 ∧ Tr 𝑧 ∧ ∀ 𝑡 ∈ 𝑧 ¬ 𝑡 ∈ 𝑡 ) }
64 58 63 elab2g ⊢ ( suc ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ¬ 𝑡 ∈ 𝑡 ) } ∈ V → ( suc ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ¬ 𝑡 ∈ 𝑡 ) } ∈ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ¬ 𝑡 ∈ 𝑡 ) } ↔ ( suc ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ¬ 𝑡 ∈ 𝑡 ) } ⊆ 𝐴 ∧ Tr suc ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ¬ 𝑡 ∈ 𝑡 ) } ∧ ∀ 𝑡 ∈ suc ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ¬ 𝑡 ∈ 𝑡 ) } ¬ 𝑡 ∈ 𝑡 ) ) )
65 64 biimprd ⊢ ( suc ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ¬ 𝑡 ∈ 𝑡 ) } ∈ V → ( ( suc ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ¬ 𝑡 ∈ 𝑡 ) } ⊆ 𝐴 ∧ Tr suc ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ¬ 𝑡 ∈ 𝑡 ) } ∧ ∀ 𝑡 ∈ suc ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ¬ 𝑡 ∈ 𝑡 ) } ¬ 𝑡 ∈ 𝑡 ) → suc ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ¬ 𝑡 ∈ 𝑡 ) } ∈ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ¬ 𝑡 ∈ 𝑡 ) } ) )
66 sucexg ⊢ ( ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ¬ 𝑡 ∈ 𝑡 ) } ∈ 𝐴 → suc ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ¬ 𝑡 ∈ 𝑡 ) } ∈ V )
67 65 66 syl11 ⊢ ( ( suc ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ¬ 𝑡 ∈ 𝑡 ) } ⊆ 𝐴 ∧ Tr suc ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ¬ 𝑡 ∈ 𝑡 ) } ∧ ∀ 𝑡 ∈ suc ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ¬ 𝑡 ∈ 𝑡 ) } ¬ 𝑡 ∈ 𝑡 ) → ( ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ¬ 𝑡 ∈ 𝑡 ) } ∈ 𝐴 → suc ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ¬ 𝑡 ∈ 𝑡 ) } ∈ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ¬ 𝑡 ∈ 𝑡 ) } ) )
68 42 52 67 mp3an23 ⊢ ( suc ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ¬ 𝑡 ∈ 𝑡 ) } ⊆ 𝐴 → ( ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ¬ 𝑡 ∈ 𝑡 ) } ∈ 𝐴 → suc ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ¬ 𝑡 ∈ 𝑡 ) } ∈ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ¬ 𝑡 ∈ 𝑡 ) } ) )
69 68 com12 ⊢ ( ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ¬ 𝑡 ∈ 𝑡 ) } ∈ 𝐴 → ( suc ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ¬ 𝑡 ∈ 𝑡 ) } ⊆ 𝐴 → suc ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ¬ 𝑡 ∈ 𝑡 ) } ∈ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ¬ 𝑡 ∈ 𝑡 ) } ) )
70 elssuni ⊢ ( suc ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ¬ 𝑡 ∈ 𝑡 ) } ∈ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ¬ 𝑡 ∈ 𝑡 ) } → suc ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ¬ 𝑡 ∈ 𝑡 ) } ⊆ ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ¬ 𝑡 ∈ 𝑡 ) } )
71 sucssel ⊢ ( ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ¬ 𝑡 ∈ 𝑡 ) } ∈ 𝐴 → ( suc ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ¬ 𝑡 ∈ 𝑡 ) } ⊆ ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ¬ 𝑡 ∈ 𝑡 ) } → ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ¬ 𝑡 ∈ 𝑡 ) } ∈ ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ¬ 𝑡 ∈ 𝑡 ) } ) )
72 70 71 syl5 ⊢ ( ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ¬ 𝑡 ∈ 𝑡 ) } ∈ 𝐴 → ( suc ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ¬ 𝑡 ∈ 𝑡 ) } ∈ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ¬ 𝑡 ∈ 𝑡 ) } → ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ¬ 𝑡 ∈ 𝑡 ) } ∈ ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ¬ 𝑡 ∈ 𝑡 ) } ) )
73 69 72 syld ⊢ ( ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ¬ 𝑡 ∈ 𝑡 ) } ∈ 𝐴 → ( suc ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ¬ 𝑡 ∈ 𝑡 ) } ⊆ 𝐴 → ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ¬ 𝑡 ∈ 𝑡 ) } ∈ ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ¬ 𝑡 ∈ 𝑡 ) } ) )
74 40 73 mpd ⊢ ( ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ¬ 𝑡 ∈ 𝑡 ) } ∈ 𝐴 → ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ¬ 𝑡 ∈ 𝑡 ) } ∈ ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ¬ 𝑡 ∈ 𝑡 ) } )
75 34 74 syl6 ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ∀ 𝑥 ( ( 𝑥 ⊊ 𝐴 ∧ Tr 𝑥 ) → 𝑥 ∈ 𝐴 ) ) → ( ( ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ¬ 𝑡 ∈ 𝑡 ) } ⊊ 𝐴 ∧ Tr ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ¬ 𝑡 ∈ 𝑡 ) } ) → ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ¬ 𝑡 ∈ 𝑡 ) } ∈ ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ¬ 𝑡 ∈ 𝑡 ) } ) )
76 24 75 mpan2i ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ∀ 𝑥 ( ( 𝑥 ⊊ 𝐴 ∧ Tr 𝑥 ) → 𝑥 ∈ 𝐴 ) ) → ( ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ¬ 𝑡 ∈ 𝑡 ) } ⊊ 𝐴 → ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ¬ 𝑡 ∈ 𝑡 ) } ∈ ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ¬ 𝑡 ∈ 𝑡 ) } ) )
77 23 76 biimtrrid ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ∀ 𝑥 ( ( 𝑥 ⊊ 𝐴 ∧ Tr 𝑥 ) → 𝑥 ∈ 𝐴 ) ) → ( ( ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ¬ 𝑡 ∈ 𝑡 ) } ⊆ 𝐴 ∧ ¬ ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ¬ 𝑡 ∈ 𝑡 ) } = 𝐴 ) → ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ¬ 𝑡 ∈ 𝑡 ) } ∈ ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ¬ 𝑡 ∈ 𝑡 ) } ) )
78 22 77 mpani ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ∀ 𝑥 ( ( 𝑥 ⊊ 𝐴 ∧ Tr 𝑥 ) → 𝑥 ∈ 𝐴 ) ) → ( ¬ ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ¬ 𝑡 ∈ 𝑡 ) } = 𝐴 → ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ¬ 𝑡 ∈ 𝑡 ) } ∈ ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ¬ 𝑡 ∈ 𝑡 ) } ) )
79 21 78 mt3i ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ∀ 𝑥 ( ( 𝑥 ⊊ 𝐴 ∧ Tr 𝑥 ) → 𝑥 ∈ 𝐴 ) ) → ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ¬ 𝑡 ∈ 𝑡 ) } = 𝐴 )
80 24 44 pm3.2i ⊢ ( Tr ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ¬ 𝑡 ∈ 𝑡 ) } ∧ ∀ 𝑧 ∈ ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ¬ 𝑡 ∈ 𝑡 ) } ¬ 𝑧 ∈ 𝑧 )
81 treq ⊢ ( ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ¬ 𝑡 ∈ 𝑡 ) } = 𝐴 → ( Tr ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ¬ 𝑡 ∈ 𝑡 ) } ↔ Tr 𝐴 ) )
82 raleq ⊢ ( ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ¬ 𝑡 ∈ 𝑡 ) } = 𝐴 → ( ∀ 𝑧 ∈ ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ¬ 𝑡 ∈ 𝑡 ) } ¬ 𝑧 ∈ 𝑧 ↔ ∀ 𝑧 ∈ 𝐴 ¬ 𝑧 ∈ 𝑧 ) )
83 81 82 anbi12d ⊢ ( ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ¬ 𝑡 ∈ 𝑡 ) } = 𝐴 → ( ( Tr ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ¬ 𝑡 ∈ 𝑡 ) } ∧ ∀ 𝑧 ∈ ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ¬ 𝑡 ∈ 𝑡 ) } ¬ 𝑧 ∈ 𝑧 ) ↔ ( Tr 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ¬ 𝑧 ∈ 𝑧 ) ) )
84 80 83 mpbii ⊢ ( ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ¬ 𝑡 ∈ 𝑡 ) } = 𝐴 → ( Tr 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ¬ 𝑧 ∈ 𝑧 ) )
85 79 84 syl ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ∀ 𝑥 ( ( 𝑥 ⊊ 𝐴 ∧ Tr 𝑥 ) → 𝑥 ∈ 𝐴 ) ) → ( Tr 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ¬ 𝑧 ∈ 𝑧 ) )
86 85 ex ⊢ ( 𝐴 ∈ 𝑉 → ( ∀ 𝑥 ( ( 𝑥 ⊊ 𝐴 ∧ Tr 𝑥 ) → 𝑥 ∈ 𝐴 ) → ( Tr 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ¬ 𝑧 ∈ 𝑧 ) ) )