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 ⊢ ∃ y ∀ z z = x ∨ z ∈ y → ∀ x x ∈ z → x ∈ y

Proof

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