Metamath Proof Explorer

Theorem axtcond

Description: A version of the Axiom of Transitive Containment with no distinct variable conditions. Usage of this theorem is discouraged because it depends on ax-13 . (Contributed by Matthew House, 6-Apr-2026) (New usage is discouraged.)

Ref Expression
Assertion axtcond ∃ 𝑦 ∀ 𝑧 ( ( 𝑧 = 𝑥 ∨ 𝑧 ∈ 𝑦 ) → ∀ 𝑥 ( 𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑦 ) )

Proof

Step Hyp Ref Expression
1 axtco2 ⊢ ∃ 𝑤 ∀ 𝑣 ( ( 𝑣 = 𝑥 ∨ 𝑣 ∈ 𝑤 ) → ∀ 𝑥 ( 𝑥 ∈ 𝑣 → 𝑥 ∈ 𝑤 ) )
2 nfnae ⊢ Ⅎ 𝑦 ¬ ∀ 𝑥 𝑥 = 𝑦
3 nfnae ⊢ Ⅎ 𝑦 ¬ ∀ 𝑥 𝑥 = 𝑧
4 nfnae ⊢ Ⅎ 𝑦 ¬ ∀ 𝑦 𝑦 = 𝑧
5 2 3 4 nf3an ⊢ Ⅎ 𝑦 ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ ¬ ∀ 𝑥 𝑥 = 𝑧 ∧ ¬ ∀ 𝑦 𝑦 = 𝑧 )
6 nfv ⊢ Ⅎ 𝑦 ∀ 𝑣 ( ( 𝑣 = 𝑡 ∨ 𝑣 ∈ 𝑤 ) → ∀ 𝑡 ( 𝑡 ∈ 𝑣 → 𝑡 ∈ 𝑤 ) )
7 equequ2 ⊢ ( 𝑡 = 𝑥 → ( 𝑣 = 𝑡 ↔ 𝑣 = 𝑥 ) )
8 7 orbi1d ⊢ ( 𝑡 = 𝑥 → ( ( 𝑣 = 𝑡 ∨ 𝑣 ∈ 𝑤 ) ↔ ( 𝑣 = 𝑥 ∨ 𝑣 ∈ 𝑤 ) ) )
9 elequ1 ⊢ ( 𝑡 = 𝑥 → ( 𝑡 ∈ 𝑣 ↔ 𝑥 ∈ 𝑣 ) )
10 elequ1 ⊢ ( 𝑡 = 𝑥 → ( 𝑡 ∈ 𝑤 ↔ 𝑥 ∈ 𝑤 ) )
11 9 10 imbi12d ⊢ ( 𝑡 = 𝑥 → ( ( 𝑡 ∈ 𝑣 → 𝑡 ∈ 𝑤 ) ↔ ( 𝑥 ∈ 𝑣 → 𝑥 ∈ 𝑤 ) ) )
12 11 cbvalvw ⊢ ( ∀ 𝑡 ( 𝑡 ∈ 𝑣 → 𝑡 ∈ 𝑤 ) ↔ ∀ 𝑥 ( 𝑥 ∈ 𝑣 → 𝑥 ∈ 𝑤 ) )
13 12 a1i ⊢ ( 𝑡 = 𝑥 → ( ∀ 𝑡 ( 𝑡 ∈ 𝑣 → 𝑡 ∈ 𝑤 ) ↔ ∀ 𝑥 ( 𝑥 ∈ 𝑣 → 𝑥 ∈ 𝑤 ) ) )
14 8 13 imbi12d ⊢ ( 𝑡 = 𝑥 → ( ( ( 𝑣 = 𝑡 ∨ 𝑣 ∈ 𝑤 ) → ∀ 𝑡 ( 𝑡 ∈ 𝑣 → 𝑡 ∈ 𝑤 ) ) ↔ ( ( 𝑣 = 𝑥 ∨ 𝑣 ∈ 𝑤 ) → ∀ 𝑥 ( 𝑥 ∈ 𝑣 → 𝑥 ∈ 𝑤 ) ) ) )
15 14 albidv ⊢ ( 𝑡 = 𝑥 → ( ∀ 𝑣 ( ( 𝑣 = 𝑡 ∨ 𝑣 ∈ 𝑤 ) → ∀ 𝑡 ( 𝑡 ∈ 𝑣 → 𝑡 ∈ 𝑤 ) ) ↔ ∀ 𝑣 ( ( 𝑣 = 𝑥 ∨ 𝑣 ∈ 𝑤 ) → ∀ 𝑥 ( 𝑥 ∈ 𝑣 → 𝑥 ∈ 𝑤 ) ) ) )
16 6 15 dvelimnf ⊢ ( ¬ ∀ 𝑦 𝑦 = 𝑥 → Ⅎ 𝑦 ∀ 𝑣 ( ( 𝑣 = 𝑥 ∨ 𝑣 ∈ 𝑤 ) → ∀ 𝑥 ( 𝑥 ∈ 𝑣 → 𝑥 ∈ 𝑤 ) ) )
17 16 naecoms ⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → Ⅎ 𝑦 ∀ 𝑣 ( ( 𝑣 = 𝑥 ∨ 𝑣 ∈ 𝑤 ) → ∀ 𝑥 ( 𝑥 ∈ 𝑣 → 𝑥 ∈ 𝑤 ) ) )
18 17 3ad2ant1 ⊢ ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ ¬ ∀ 𝑥 𝑥 = 𝑧 ∧ ¬ ∀ 𝑦 𝑦 = 𝑧 ) → Ⅎ 𝑦 ∀ 𝑣 ( ( 𝑣 = 𝑥 ∨ 𝑣 ∈ 𝑤 ) → ∀ 𝑥 ( 𝑥 ∈ 𝑣 → 𝑥 ∈ 𝑤 ) ) )
19 nfnae ⊢ Ⅎ 𝑧 ¬ ∀ 𝑥 𝑥 = 𝑦
20 nfnae ⊢ Ⅎ 𝑧 ¬ ∀ 𝑥 𝑥 = 𝑧
21 nfnae ⊢ Ⅎ 𝑧 ¬ ∀ 𝑦 𝑦 = 𝑧
22 19 20 21 nf3an ⊢ Ⅎ 𝑧 ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ ¬ ∀ 𝑥 𝑥 = 𝑧 ∧ ¬ ∀ 𝑦 𝑦 = 𝑧 )
23 nfeqf2 ⊢ ( ¬ ∀ 𝑧 𝑧 = 𝑦 → Ⅎ 𝑧 𝑤 = 𝑦 )
24 23 naecoms ⊢ ( ¬ ∀ 𝑦 𝑦 = 𝑧 → Ⅎ 𝑧 𝑤 = 𝑦 )
25 24 3ad2ant3 ⊢ ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ ¬ ∀ 𝑥 𝑥 = 𝑧 ∧ ¬ ∀ 𝑦 𝑦 = 𝑧 ) → Ⅎ 𝑧 𝑤 = 𝑦 )
26 22 25 nfan1 ⊢ Ⅎ 𝑧 ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ ¬ ∀ 𝑥 𝑥 = 𝑧 ∧ ¬ ∀ 𝑦 𝑦 = 𝑧 ) ∧ 𝑤 = 𝑦 )
27 simpl2 ⊢ ( ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ ¬ ∀ 𝑥 𝑥 = 𝑧 ∧ ¬ ∀ 𝑦 𝑦 = 𝑧 ) ∧ 𝑤 = 𝑦 ) → ¬ ∀ 𝑥 𝑥 = 𝑧 )
28 nfv ⊢ Ⅎ 𝑧 ( ( 𝑣 = 𝑡 ∨ 𝑣 ∈ 𝑤 ) → ∀ 𝑡 ( 𝑡 ∈ 𝑣 → 𝑡 ∈ 𝑤 ) )
29 28 14 dvelimnf ⊢ ( ¬ ∀ 𝑧 𝑧 = 𝑥 → Ⅎ 𝑧 ( ( 𝑣 = 𝑥 ∨ 𝑣 ∈ 𝑤 ) → ∀ 𝑥 ( 𝑥 ∈ 𝑣 → 𝑥 ∈ 𝑤 ) ) )
30 29 naecoms ⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑧 → Ⅎ 𝑧 ( ( 𝑣 = 𝑥 ∨ 𝑣 ∈ 𝑤 ) → ∀ 𝑥 ( 𝑥 ∈ 𝑣 → 𝑥 ∈ 𝑤 ) ) )
31 27 30 syl ⊢ ( ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ ¬ ∀ 𝑥 𝑥 = 𝑧 ∧ ¬ ∀ 𝑦 𝑦 = 𝑧 ) ∧ 𝑤 = 𝑦 ) → Ⅎ 𝑧 ( ( 𝑣 = 𝑥 ∨ 𝑣 ∈ 𝑤 ) → ∀ 𝑥 ( 𝑥 ∈ 𝑣 → 𝑥 ∈ 𝑤 ) ) )
32 equequ1 ⊢ ( 𝑣 = 𝑧 → ( 𝑣 = 𝑥 ↔ 𝑧 = 𝑥 ) )
33 32 adantl ⊢ ( ( 𝑤 = 𝑦 ∧ 𝑣 = 𝑧 ) → ( 𝑣 = 𝑥 ↔ 𝑧 = 𝑥 ) )
34 elequ12 ⊢ ( ( 𝑣 = 𝑧 ∧ 𝑤 = 𝑦 ) → ( 𝑣 ∈ 𝑤 ↔ 𝑧 ∈ 𝑦 ) )
35 34 ancoms ⊢ ( ( 𝑤 = 𝑦 ∧ 𝑣 = 𝑧 ) → ( 𝑣 ∈ 𝑤 ↔ 𝑧 ∈ 𝑦 ) )
36 33 35 orbi12d ⊢ ( ( 𝑤 = 𝑦 ∧ 𝑣 = 𝑧 ) → ( ( 𝑣 = 𝑥 ∨ 𝑣 ∈ 𝑤 ) ↔ ( 𝑧 = 𝑥 ∨ 𝑧 ∈ 𝑦 ) ) )
37 36 adantl ⊢ ( ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ ¬ ∀ 𝑥 𝑥 = 𝑧 ) ∧ ( 𝑤 = 𝑦 ∧ 𝑣 = 𝑧 ) ) → ( ( 𝑣 = 𝑥 ∨ 𝑣 ∈ 𝑤 ) ↔ ( 𝑧 = 𝑥 ∨ 𝑧 ∈ 𝑦 ) ) )
38 nfnae ⊢ Ⅎ 𝑥 ¬ ∀ 𝑥 𝑥 = 𝑦
39 nfnae ⊢ Ⅎ 𝑥 ¬ ∀ 𝑥 𝑥 = 𝑧
40 38 39 nfan ⊢ Ⅎ 𝑥 ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ ¬ ∀ 𝑥 𝑥 = 𝑧 )
41 nfeqf2 ⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → Ⅎ 𝑥 𝑤 = 𝑦 )
42 41 adantr ⊢ ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ ¬ ∀ 𝑥 𝑥 = 𝑧 ) → Ⅎ 𝑥 𝑤 = 𝑦 )
43 nfeqf2 ⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑧 → Ⅎ 𝑥 𝑣 = 𝑧 )
44 43 adantl ⊢ ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ ¬ ∀ 𝑥 𝑥 = 𝑧 ) → Ⅎ 𝑥 𝑣 = 𝑧 )
45 42 44 nfand ⊢ ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ ¬ ∀ 𝑥 𝑥 = 𝑧 ) → Ⅎ 𝑥 ( 𝑤 = 𝑦 ∧ 𝑣 = 𝑧 ) )
46 40 45 nfan1 ⊢ Ⅎ 𝑥 ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ ¬ ∀ 𝑥 𝑥 = 𝑧 ) ∧ ( 𝑤 = 𝑦 ∧ 𝑣 = 𝑧 ) )
47 elequ2 ⊢ ( 𝑣 = 𝑧 → ( 𝑥 ∈ 𝑣 ↔ 𝑥 ∈ 𝑧 ) )
48 47 adantl ⊢ ( ( 𝑤 = 𝑦 ∧ 𝑣 = 𝑧 ) → ( 𝑥 ∈ 𝑣 ↔ 𝑥 ∈ 𝑧 ) )
49 elequ2 ⊢ ( 𝑤 = 𝑦 → ( 𝑥 ∈ 𝑤 ↔ 𝑥 ∈ 𝑦 ) )
50 49 adantr ⊢ ( ( 𝑤 = 𝑦 ∧ 𝑣 = 𝑧 ) → ( 𝑥 ∈ 𝑤 ↔ 𝑥 ∈ 𝑦 ) )
51 48 50 imbi12d ⊢ ( ( 𝑤 = 𝑦 ∧ 𝑣 = 𝑧 ) → ( ( 𝑥 ∈ 𝑣 → 𝑥 ∈ 𝑤 ) ↔ ( 𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑦 ) ) )
52 51 adantl ⊢ ( ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ ¬ ∀ 𝑥 𝑥 = 𝑧 ) ∧ ( 𝑤 = 𝑦 ∧ 𝑣 = 𝑧 ) ) → ( ( 𝑥 ∈ 𝑣 → 𝑥 ∈ 𝑤 ) ↔ ( 𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑦 ) ) )
53 46 52 albid ⊢ ( ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ ¬ ∀ 𝑥 𝑥 = 𝑧 ) ∧ ( 𝑤 = 𝑦 ∧ 𝑣 = 𝑧 ) ) → ( ∀ 𝑥 ( 𝑥 ∈ 𝑣 → 𝑥 ∈ 𝑤 ) ↔ ∀ 𝑥 ( 𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑦 ) ) )
54 37 53 imbi12d ⊢ ( ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ ¬ ∀ 𝑥 𝑥 = 𝑧 ) ∧ ( 𝑤 = 𝑦 ∧ 𝑣 = 𝑧 ) ) → ( ( ( 𝑣 = 𝑥 ∨ 𝑣 ∈ 𝑤 ) → ∀ 𝑥 ( 𝑥 ∈ 𝑣 → 𝑥 ∈ 𝑤 ) ) ↔ ( ( 𝑧 = 𝑥 ∨ 𝑧 ∈ 𝑦 ) → ∀ 𝑥 ( 𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑦 ) ) ) )
55 54 expr ⊢ ( ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ ¬ ∀ 𝑥 𝑥 = 𝑧 ) ∧ 𝑤 = 𝑦 ) → ( 𝑣 = 𝑧 → ( ( ( 𝑣 = 𝑥 ∨ 𝑣 ∈ 𝑤 ) → ∀ 𝑥 ( 𝑥 ∈ 𝑣 → 𝑥 ∈ 𝑤 ) ) ↔ ( ( 𝑧 = 𝑥 ∨ 𝑧 ∈ 𝑦 ) → ∀ 𝑥 ( 𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑦 ) ) ) ) )
56 55 3adantl3 ⊢ ( ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ ¬ ∀ 𝑥 𝑥 = 𝑧 ∧ ¬ ∀ 𝑦 𝑦 = 𝑧 ) ∧ 𝑤 = 𝑦 ) → ( 𝑣 = 𝑧 → ( ( ( 𝑣 = 𝑥 ∨ 𝑣 ∈ 𝑤 ) → ∀ 𝑥 ( 𝑥 ∈ 𝑣 → 𝑥 ∈ 𝑤 ) ) ↔ ( ( 𝑧 = 𝑥 ∨ 𝑧 ∈ 𝑦 ) → ∀ 𝑥 ( 𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑦 ) ) ) ) )
57 26 31 56 cbvaldw ⊢ ( ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ ¬ ∀ 𝑥 𝑥 = 𝑧 ∧ ¬ ∀ 𝑦 𝑦 = 𝑧 ) ∧ 𝑤 = 𝑦 ) → ( ∀ 𝑣 ( ( 𝑣 = 𝑥 ∨ 𝑣 ∈ 𝑤 ) → ∀ 𝑥 ( 𝑥 ∈ 𝑣 → 𝑥 ∈ 𝑤 ) ) ↔ ∀ 𝑧 ( ( 𝑧 = 𝑥 ∨ 𝑧 ∈ 𝑦 ) → ∀ 𝑥 ( 𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑦 ) ) ) )
58 57 ex ⊢ ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ ¬ ∀ 𝑥 𝑥 = 𝑧 ∧ ¬ ∀ 𝑦 𝑦 = 𝑧 ) → ( 𝑤 = 𝑦 → ( ∀ 𝑣 ( ( 𝑣 = 𝑥 ∨ 𝑣 ∈ 𝑤 ) → ∀ 𝑥 ( 𝑥 ∈ 𝑣 → 𝑥 ∈ 𝑤 ) ) ↔ ∀ 𝑧 ( ( 𝑧 = 𝑥 ∨ 𝑧 ∈ 𝑦 ) → ∀ 𝑥 ( 𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑦 ) ) ) ) )
59 5 18 58 cbvexdw ⊢ ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ ¬ ∀ 𝑥 𝑥 = 𝑧 ∧ ¬ ∀ 𝑦 𝑦 = 𝑧 ) → ( ∃ 𝑤 ∀ 𝑣 ( ( 𝑣 = 𝑥 ∨ 𝑣 ∈ 𝑤 ) → ∀ 𝑥 ( 𝑥 ∈ 𝑣 → 𝑥 ∈ 𝑤 ) ) ↔ ∃ 𝑦 ∀ 𝑧 ( ( 𝑧 = 𝑥 ∨ 𝑧 ∈ 𝑦 ) → ∀ 𝑥 ( 𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑦 ) ) ) )
60 1 59 mpbii ⊢ ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ ¬ ∀ 𝑥 𝑥 = 𝑧 ∧ ¬ ∀ 𝑦 𝑦 = 𝑧 ) → ∃ 𝑦 ∀ 𝑧 ( ( 𝑧 = 𝑥 ∨ 𝑧 ∈ 𝑦 ) → ∀ 𝑥 ( 𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑦 ) ) )
61 60 3exp ⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → ( ¬ ∀ 𝑥 𝑥 = 𝑧 → ( ¬ ∀ 𝑦 𝑦 = 𝑧 → ∃ 𝑦 ∀ 𝑧 ( ( 𝑧 = 𝑥 ∨ 𝑧 ∈ 𝑦 ) → ∀ 𝑥 ( 𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑦 ) ) ) ) )
62 nfae ⊢ Ⅎ 𝑧 ∀ 𝑦 𝑦 = 𝑧
63 nfae ⊢ Ⅎ 𝑥 ∀ 𝑦 𝑦 = 𝑧
64 elequ2 ⊢ ( 𝑦 = 𝑧 → ( 𝑥 ∈ 𝑦 ↔ 𝑥 ∈ 𝑧 ) )
65 64 sps ⊢ ( ∀ 𝑦 𝑦 = 𝑧 → ( 𝑥 ∈ 𝑦 ↔ 𝑥 ∈ 𝑧 ) )
66 65 biimprd ⊢ ( ∀ 𝑦 𝑦 = 𝑧 → ( 𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑦 ) )
67 63 66 alrimi ⊢ ( ∀ 𝑦 𝑦 = 𝑧 → ∀ 𝑥 ( 𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑦 ) )
68 67 a1d ⊢ ( ∀ 𝑦 𝑦 = 𝑧 → ( ( 𝑧 = 𝑥 ∨ 𝑧 ∈ 𝑦 ) → ∀ 𝑥 ( 𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑦 ) ) )
69 62 68 alrimi ⊢ ( ∀ 𝑦 𝑦 = 𝑧 → ∀ 𝑧 ( ( 𝑧 = 𝑥 ∨ 𝑧 ∈ 𝑦 ) → ∀ 𝑥 ( 𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑦 ) ) )
70 69 19.8ad ⊢ ( ∀ 𝑦 𝑦 = 𝑧 → ∃ 𝑦 ∀ 𝑧 ( ( 𝑧 = 𝑥 ∨ 𝑧 ∈ 𝑦 ) → ∀ 𝑥 ( 𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑦 ) ) )
71 70 a1i ⊢ ( ∀ 𝑥 𝑥 = 𝑦 → ( ∀ 𝑦 𝑦 = 𝑧 → ∃ 𝑦 ∀ 𝑧 ( ( 𝑧 = 𝑥 ∨ 𝑧 ∈ 𝑦 ) → ∀ 𝑥 ( 𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑦 ) ) ) )
72 ax-nul ⊢ ∃ 𝑦 ∀ 𝑢 ¬ 𝑢 ∈ 𝑦
73 nfv ⊢ Ⅎ 𝑧 ∀ 𝑢 ¬ 𝑢 ∈ 𝑡
74 elequ2 ⊢ ( 𝑡 = 𝑦 → ( 𝑢 ∈ 𝑡 ↔ 𝑢 ∈ 𝑦 ) )
75 74 notbid ⊢ ( 𝑡 = 𝑦 → ( ¬ 𝑢 ∈ 𝑡 ↔ ¬ 𝑢 ∈ 𝑦 ) )
76 75 albidv ⊢ ( 𝑡 = 𝑦 → ( ∀ 𝑢 ¬ 𝑢 ∈ 𝑡 ↔ ∀ 𝑢 ¬ 𝑢 ∈ 𝑦 ) )
77 73 76 dvelimnf ⊢ ( ¬ ∀ 𝑧 𝑧 = 𝑦 → Ⅎ 𝑧 ∀ 𝑢 ¬ 𝑢 ∈ 𝑦 )
78 77 naecoms ⊢ ( ¬ ∀ 𝑦 𝑦 = 𝑧 → Ⅎ 𝑧 ∀ 𝑢 ¬ 𝑢 ∈ 𝑦 )
79 elequ2 ⊢ ( 𝑧 = 𝑦 → ( 𝑢 ∈ 𝑧 ↔ 𝑢 ∈ 𝑦 ) )
80 79 notbid ⊢ ( 𝑧 = 𝑦 → ( ¬ 𝑢 ∈ 𝑧 ↔ ¬ 𝑢 ∈ 𝑦 ) )
81 80 albidv ⊢ ( 𝑧 = 𝑦 → ( ∀ 𝑢 ¬ 𝑢 ∈ 𝑧 ↔ ∀ 𝑢 ¬ 𝑢 ∈ 𝑦 ) )
82 81 biimprcd ⊢ ( ∀ 𝑢 ¬ 𝑢 ∈ 𝑦 → ( 𝑧 = 𝑦 → ∀ 𝑢 ¬ 𝑢 ∈ 𝑧 ) )
83 elirrv ⊢ ¬ 𝑥 ∈ 𝑥
84 elequ2 ⊢ ( 𝑥 = 𝑧 → ( 𝑥 ∈ 𝑥 ↔ 𝑥 ∈ 𝑧 ) )
85 83 84 mtbii ⊢ ( 𝑥 = 𝑧 → ¬ 𝑥 ∈ 𝑧 )
86 85 pm2.21d ⊢ ( 𝑥 = 𝑧 → ( 𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑦 ) )
87 86 alimi ⊢ ( ∀ 𝑥 𝑥 = 𝑧 → ∀ 𝑥 ( 𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑦 ) )
88 87 a1d ⊢ ( ∀ 𝑥 𝑥 = 𝑧 → ( ∀ 𝑢 ¬ 𝑢 ∈ 𝑧 → ∀ 𝑥 ( 𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑦 ) ) )
89 nfv ⊢ Ⅎ 𝑥 ∀ 𝑢 ¬ 𝑢 ∈ 𝑡
90 elequ2 ⊢ ( 𝑡 = 𝑧 → ( 𝑢 ∈ 𝑡 ↔ 𝑢 ∈ 𝑧 ) )
91 90 notbid ⊢ ( 𝑡 = 𝑧 → ( ¬ 𝑢 ∈ 𝑡 ↔ ¬ 𝑢 ∈ 𝑧 ) )
92 91 albidv ⊢ ( 𝑡 = 𝑧 → ( ∀ 𝑢 ¬ 𝑢 ∈ 𝑡 ↔ ∀ 𝑢 ¬ 𝑢 ∈ 𝑧 ) )
93 89 92 dvelimnf ⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑧 → Ⅎ 𝑥 ∀ 𝑢 ¬ 𝑢 ∈ 𝑧 )
94 elequ1 ⊢ ( 𝑢 = 𝑥 → ( 𝑢 ∈ 𝑧 ↔ 𝑥 ∈ 𝑧 ) )
95 94 notbid ⊢ ( 𝑢 = 𝑥 → ( ¬ 𝑢 ∈ 𝑧 ↔ ¬ 𝑥 ∈ 𝑧 ) )
96 95 spvv ⊢ ( ∀ 𝑢 ¬ 𝑢 ∈ 𝑧 → ¬ 𝑥 ∈ 𝑧 )
97 96 pm2.21d ⊢ ( ∀ 𝑢 ¬ 𝑢 ∈ 𝑧 → ( 𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑦 ) )
98 97 a1i ⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑧 → ( ∀ 𝑢 ¬ 𝑢 ∈ 𝑧 → ( 𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑦 ) ) )
99 39 93 98 alrimdd ⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑧 → ( ∀ 𝑢 ¬ 𝑢 ∈ 𝑧 → ∀ 𝑥 ( 𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑦 ) ) )
100 88 99 pm2.61i ⊢ ( ∀ 𝑢 ¬ 𝑢 ∈ 𝑧 → ∀ 𝑥 ( 𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑦 ) )
101 82 100 syl6 ⊢ ( ∀ 𝑢 ¬ 𝑢 ∈ 𝑦 → ( 𝑧 = 𝑦 → ∀ 𝑥 ( 𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑦 ) ) )
102 elequ1 ⊢ ( 𝑢 = 𝑧 → ( 𝑢 ∈ 𝑦 ↔ 𝑧 ∈ 𝑦 ) )
103 102 notbid ⊢ ( 𝑢 = 𝑧 → ( ¬ 𝑢 ∈ 𝑦 ↔ ¬ 𝑧 ∈ 𝑦 ) )
104 103 spvv ⊢ ( ∀ 𝑢 ¬ 𝑢 ∈ 𝑦 → ¬ 𝑧 ∈ 𝑦 )
105 104 pm2.21d ⊢ ( ∀ 𝑢 ¬ 𝑢 ∈ 𝑦 → ( 𝑧 ∈ 𝑦 → ∀ 𝑥 ( 𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑦 ) ) )
106 101 105 jaod ⊢ ( ∀ 𝑢 ¬ 𝑢 ∈ 𝑦 → ( ( 𝑧 = 𝑦 ∨ 𝑧 ∈ 𝑦 ) → ∀ 𝑥 ( 𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑦 ) ) )
107 106 a1i ⊢ ( ¬ ∀ 𝑦 𝑦 = 𝑧 → ( ∀ 𝑢 ¬ 𝑢 ∈ 𝑦 → ( ( 𝑧 = 𝑦 ∨ 𝑧 ∈ 𝑦 ) → ∀ 𝑥 ( 𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑦 ) ) ) )
108 21 78 107 alrimdd ⊢ ( ¬ ∀ 𝑦 𝑦 = 𝑧 → ( ∀ 𝑢 ¬ 𝑢 ∈ 𝑦 → ∀ 𝑧 ( ( 𝑧 = 𝑦 ∨ 𝑧 ∈ 𝑦 ) → ∀ 𝑥 ( 𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑦 ) ) ) )
109 4 108 eximd ⊢ ( ¬ ∀ 𝑦 𝑦 = 𝑧 → ( ∃ 𝑦 ∀ 𝑢 ¬ 𝑢 ∈ 𝑦 → ∃ 𝑦 ∀ 𝑧 ( ( 𝑧 = 𝑦 ∨ 𝑧 ∈ 𝑦 ) → ∀ 𝑥 ( 𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑦 ) ) ) )
110 72 109 mpi ⊢ ( ¬ ∀ 𝑦 𝑦 = 𝑧 → ∃ 𝑦 ∀ 𝑧 ( ( 𝑧 = 𝑦 ∨ 𝑧 ∈ 𝑦 ) → ∀ 𝑥 ( 𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑦 ) ) )
111 nfae ⊢ Ⅎ 𝑦 ∀ 𝑥 𝑥 = 𝑦
112 nfae ⊢ Ⅎ 𝑧 ∀ 𝑥 𝑥 = 𝑦
113 equequ2 ⊢ ( 𝑥 = 𝑦 → ( 𝑧 = 𝑥 ↔ 𝑧 = 𝑦 ) )
114 113 sps ⊢ ( ∀ 𝑥 𝑥 = 𝑦 → ( 𝑧 = 𝑥 ↔ 𝑧 = 𝑦 ) )
115 114 orbi1d ⊢ ( ∀ 𝑥 𝑥 = 𝑦 → ( ( 𝑧 = 𝑥 ∨ 𝑧 ∈ 𝑦 ) ↔ ( 𝑧 = 𝑦 ∨ 𝑧 ∈ 𝑦 ) ) )
116 115 imbi1d ⊢ ( ∀ 𝑥 𝑥 = 𝑦 → ( ( ( 𝑧 = 𝑥 ∨ 𝑧 ∈ 𝑦 ) → ∀ 𝑥 ( 𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑦 ) ) ↔ ( ( 𝑧 = 𝑦 ∨ 𝑧 ∈ 𝑦 ) → ∀ 𝑥 ( 𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑦 ) ) ) )
117 112 116 albid ⊢ ( ∀ 𝑥 𝑥 = 𝑦 → ( ∀ 𝑧 ( ( 𝑧 = 𝑥 ∨ 𝑧 ∈ 𝑦 ) → ∀ 𝑥 ( 𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑦 ) ) ↔ ∀ 𝑧 ( ( 𝑧 = 𝑦 ∨ 𝑧 ∈ 𝑦 ) → ∀ 𝑥 ( 𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑦 ) ) ) )
118 111 117 exbid ⊢ ( ∀ 𝑥 𝑥 = 𝑦 → ( ∃ 𝑦 ∀ 𝑧 ( ( 𝑧 = 𝑥 ∨ 𝑧 ∈ 𝑦 ) → ∀ 𝑥 ( 𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑦 ) ) ↔ ∃ 𝑦 ∀ 𝑧 ( ( 𝑧 = 𝑦 ∨ 𝑧 ∈ 𝑦 ) → ∀ 𝑥 ( 𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑦 ) ) ) )
119 110 118 imbitrrid ⊢ ( ∀ 𝑥 𝑥 = 𝑦 → ( ¬ ∀ 𝑦 𝑦 = 𝑧 → ∃ 𝑦 ∀ 𝑧 ( ( 𝑧 = 𝑥 ∨ 𝑧 ∈ 𝑦 ) → ∀ 𝑥 ( 𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑦 ) ) ) )
120 71 119 pm2.61d ⊢ ( ∀ 𝑥 𝑥 = 𝑦 → ∃ 𝑦 ∀ 𝑧 ( ( 𝑧 = 𝑥 ∨ 𝑧 ∈ 𝑦 ) → ∀ 𝑥 ( 𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑦 ) ) )
121 nfae ⊢ Ⅎ 𝑧 ∀ 𝑥 𝑥 = 𝑧
122 87 a1d ⊢ ( ∀ 𝑥 𝑥 = 𝑧 → ( ( 𝑧 = 𝑥 ∨ 𝑧 ∈ 𝑦 ) → ∀ 𝑥 ( 𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑦 ) ) )
123 121 122 alrimi ⊢ ( ∀ 𝑥 𝑥 = 𝑧 → ∀ 𝑧 ( ( 𝑧 = 𝑥 ∨ 𝑧 ∈ 𝑦 ) → ∀ 𝑥 ( 𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑦 ) ) )
124 123 19.8ad ⊢ ( ∀ 𝑥 𝑥 = 𝑧 → ∃ 𝑦 ∀ 𝑧 ( ( 𝑧 = 𝑥 ∨ 𝑧 ∈ 𝑦 ) → ∀ 𝑥 ( 𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑦 ) ) )
125 61 120 124 70 pm2.61iii ⊢ ∃ 𝑦 ∀ 𝑧 ( ( 𝑧 = 𝑥 ∨ 𝑧 ∈ 𝑦 ) → ∀ 𝑥 ( 𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑦 ) )