Metamath Proof Explorer

Theorem axprALT2

Description: Alternate proof of axpr , proved from predicate calculus, ax-rep , and ax-inf2 . (Contributed by BTernaryTau, 26-Mar-2026) (Proof modification is discouraged.) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 axprlem3 ⊢ ∃ 𝑧 ∀ 𝑤 ( 𝑤 ∈ 𝑧 ↔ ∃ 𝑠 ( 𝑠 ∈ 𝑝 ∧ if- ( ∃ 𝑛 𝑛 ∈ 𝑠 , 𝑤 = 𝑥 , 𝑤 = 𝑦 ) ) )
2 elequ1 ⊢ ( 𝑡 = 𝑠 → ( 𝑡 ∈ 𝑝 ↔ 𝑠 ∈ 𝑝 ) )
3 elequ2 ⊢ ( 𝑡 = 𝑠 → ( 𝑢 ∈ 𝑡 ↔ 𝑢 ∈ 𝑠 ) )
4 2 3 anbi12d ⊢ ( 𝑡 = 𝑠 → ( ( 𝑡 ∈ 𝑝 ∧ 𝑢 ∈ 𝑡 ) ↔ ( 𝑠 ∈ 𝑝 ∧ 𝑢 ∈ 𝑠 ) ) )
5 4 cbvexvw ⊢ ( ∃ 𝑡 ( 𝑡 ∈ 𝑝 ∧ 𝑢 ∈ 𝑡 ) ↔ ∃ 𝑠 ( 𝑠 ∈ 𝑝 ∧ 𝑢 ∈ 𝑠 ) )
6 elex2 ⊢ ( 𝑢 ∈ 𝑠 → ∃ 𝑛 𝑛 ∈ 𝑠 )
7 6 anim2i ⊢ ( ( 𝑠 ∈ 𝑝 ∧ 𝑢 ∈ 𝑠 ) → ( 𝑠 ∈ 𝑝 ∧ ∃ 𝑛 𝑛 ∈ 𝑠 ) )
8 7 eximi ⊢ ( ∃ 𝑠 ( 𝑠 ∈ 𝑝 ∧ 𝑢 ∈ 𝑠 ) → ∃ 𝑠 ( 𝑠 ∈ 𝑝 ∧ ∃ 𝑛 𝑛 ∈ 𝑠 ) )
9 5 8 sylbi ⊢ ( ∃ 𝑡 ( 𝑡 ∈ 𝑝 ∧ 𝑢 ∈ 𝑡 ) → ∃ 𝑠 ( 𝑠 ∈ 𝑝 ∧ ∃ 𝑛 𝑛 ∈ 𝑠 ) )
10 9 3ad2ant3 ⊢ ( ( 𝑢 ∈ 𝑝 ∧ ∀ 𝑡 ¬ 𝑡 ∈ 𝑢 ∧ ∃ 𝑡 ( 𝑡 ∈ 𝑝 ∧ 𝑢 ∈ 𝑡 ) ) → ∃ 𝑠 ( 𝑠 ∈ 𝑝 ∧ ∃ 𝑛 𝑛 ∈ 𝑠 ) )
11 10 exlimiv ⊢ ( ∃ 𝑢 ( 𝑢 ∈ 𝑝 ∧ ∀ 𝑡 ¬ 𝑡 ∈ 𝑢 ∧ ∃ 𝑡 ( 𝑡 ∈ 𝑝 ∧ 𝑢 ∈ 𝑡 ) ) → ∃ 𝑠 ( 𝑠 ∈ 𝑝 ∧ ∃ 𝑛 𝑛 ∈ 𝑠 ) )
12 ax-1 ⊢ ( 𝑠 ∈ 𝑝 → ( 𝑤 = 𝑥 → 𝑠 ∈ 𝑝 ) )
13 ifptru ⊢ ( ∃ 𝑛 𝑛 ∈ 𝑠 → ( if- ( ∃ 𝑛 𝑛 ∈ 𝑠 , 𝑤 = 𝑥 , 𝑤 = 𝑦 ) ↔ 𝑤 = 𝑥 ) )
14 13 biimprd ⊢ ( ∃ 𝑛 𝑛 ∈ 𝑠 → ( 𝑤 = 𝑥 → if- ( ∃ 𝑛 𝑛 ∈ 𝑠 , 𝑤 = 𝑥 , 𝑤 = 𝑦 ) ) )
15 12 14 anim12ii ⊢ ( ( 𝑠 ∈ 𝑝 ∧ ∃ 𝑛 𝑛 ∈ 𝑠 ) → ( 𝑤 = 𝑥 → ( 𝑠 ∈ 𝑝 ∧ if- ( ∃ 𝑛 𝑛 ∈ 𝑠 , 𝑤 = 𝑥 , 𝑤 = 𝑦 ) ) ) )
16 15 eximi ⊢ ( ∃ 𝑠 ( 𝑠 ∈ 𝑝 ∧ ∃ 𝑛 𝑛 ∈ 𝑠 ) → ∃ 𝑠 ( 𝑤 = 𝑥 → ( 𝑠 ∈ 𝑝 ∧ if- ( ∃ 𝑛 𝑛 ∈ 𝑠 , 𝑤 = 𝑥 , 𝑤 = 𝑦 ) ) ) )
17 19.37imv ⊢ ( ∃ 𝑠 ( 𝑤 = 𝑥 → ( 𝑠 ∈ 𝑝 ∧ if- ( ∃ 𝑛 𝑛 ∈ 𝑠 , 𝑤 = 𝑥 , 𝑤 = 𝑦 ) ) ) → ( 𝑤 = 𝑥 → ∃ 𝑠 ( 𝑠 ∈ 𝑝 ∧ if- ( ∃ 𝑛 𝑛 ∈ 𝑠 , 𝑤 = 𝑥 , 𝑤 = 𝑦 ) ) ) )
18 11 16 17 3syl ⊢ ( ∃ 𝑢 ( 𝑢 ∈ 𝑝 ∧ ∀ 𝑡 ¬ 𝑡 ∈ 𝑢 ∧ ∃ 𝑡 ( 𝑡 ∈ 𝑝 ∧ 𝑢 ∈ 𝑡 ) ) → ( 𝑤 = 𝑥 → ∃ 𝑠 ( 𝑠 ∈ 𝑝 ∧ if- ( ∃ 𝑛 𝑛 ∈ 𝑠 , 𝑤 = 𝑥 , 𝑤 = 𝑦 ) ) ) )
19 3simpa ⊢ ( ( 𝑢 ∈ 𝑝 ∧ ∀ 𝑡 ¬ 𝑡 ∈ 𝑢 ∧ ∃ 𝑡 ( 𝑡 ∈ 𝑝 ∧ 𝑢 ∈ 𝑡 ) ) → ( 𝑢 ∈ 𝑝 ∧ ∀ 𝑡 ¬ 𝑡 ∈ 𝑢 ) )
20 19 eximi ⊢ ( ∃ 𝑢 ( 𝑢 ∈ 𝑝 ∧ ∀ 𝑡 ¬ 𝑡 ∈ 𝑢 ∧ ∃ 𝑡 ( 𝑡 ∈ 𝑝 ∧ 𝑢 ∈ 𝑡 ) ) → ∃ 𝑢 ( 𝑢 ∈ 𝑝 ∧ ∀ 𝑡 ¬ 𝑡 ∈ 𝑢 ) )
21 elequ1 ⊢ ( 𝑢 = 𝑠 → ( 𝑢 ∈ 𝑝 ↔ 𝑠 ∈ 𝑝 ) )
22 elequ2 ⊢ ( 𝑢 = 𝑠 → ( 𝑡 ∈ 𝑢 ↔ 𝑡 ∈ 𝑠 ) )
23 22 notbid ⊢ ( 𝑢 = 𝑠 → ( ¬ 𝑡 ∈ 𝑢 ↔ ¬ 𝑡 ∈ 𝑠 ) )
24 23 albidv ⊢ ( 𝑢 = 𝑠 → ( ∀ 𝑡 ¬ 𝑡 ∈ 𝑢 ↔ ∀ 𝑡 ¬ 𝑡 ∈ 𝑠 ) )
25 elequ1 ⊢ ( 𝑡 = 𝑛 → ( 𝑡 ∈ 𝑠 ↔ 𝑛 ∈ 𝑠 ) )
26 25 notbid ⊢ ( 𝑡 = 𝑛 → ( ¬ 𝑡 ∈ 𝑠 ↔ ¬ 𝑛 ∈ 𝑠 ) )
27 26 cbvalvw ⊢ ( ∀ 𝑡 ¬ 𝑡 ∈ 𝑠 ↔ ∀ 𝑛 ¬ 𝑛 ∈ 𝑠 )
28 24 27 bitrdi ⊢ ( 𝑢 = 𝑠 → ( ∀ 𝑡 ¬ 𝑡 ∈ 𝑢 ↔ ∀ 𝑛 ¬ 𝑛 ∈ 𝑠 ) )
29 21 28 anbi12d ⊢ ( 𝑢 = 𝑠 → ( ( 𝑢 ∈ 𝑝 ∧ ∀ 𝑡 ¬ 𝑡 ∈ 𝑢 ) ↔ ( 𝑠 ∈ 𝑝 ∧ ∀ 𝑛 ¬ 𝑛 ∈ 𝑠 ) ) )
30 29 cbvexvw ⊢ ( ∃ 𝑢 ( 𝑢 ∈ 𝑝 ∧ ∀ 𝑡 ¬ 𝑡 ∈ 𝑢 ) ↔ ∃ 𝑠 ( 𝑠 ∈ 𝑝 ∧ ∀ 𝑛 ¬ 𝑛 ∈ 𝑠 ) )
31 alnex ⊢ ( ∀ 𝑛 ¬ 𝑛 ∈ 𝑠 ↔ ¬ ∃ 𝑛 𝑛 ∈ 𝑠 )
32 31 anbi2i ⊢ ( ( 𝑠 ∈ 𝑝 ∧ ∀ 𝑛 ¬ 𝑛 ∈ 𝑠 ) ↔ ( 𝑠 ∈ 𝑝 ∧ ¬ ∃ 𝑛 𝑛 ∈ 𝑠 ) )
33 32 biimpi ⊢ ( ( 𝑠 ∈ 𝑝 ∧ ∀ 𝑛 ¬ 𝑛 ∈ 𝑠 ) → ( 𝑠 ∈ 𝑝 ∧ ¬ ∃ 𝑛 𝑛 ∈ 𝑠 ) )
34 33 eximi ⊢ ( ∃ 𝑠 ( 𝑠 ∈ 𝑝 ∧ ∀ 𝑛 ¬ 𝑛 ∈ 𝑠 ) → ∃ 𝑠 ( 𝑠 ∈ 𝑝 ∧ ¬ ∃ 𝑛 𝑛 ∈ 𝑠 ) )
35 30 34 sylbi ⊢ ( ∃ 𝑢 ( 𝑢 ∈ 𝑝 ∧ ∀ 𝑡 ¬ 𝑡 ∈ 𝑢 ) → ∃ 𝑠 ( 𝑠 ∈ 𝑝 ∧ ¬ ∃ 𝑛 𝑛 ∈ 𝑠 ) )
36 20 35 syl ⊢ ( ∃ 𝑢 ( 𝑢 ∈ 𝑝 ∧ ∀ 𝑡 ¬ 𝑡 ∈ 𝑢 ∧ ∃ 𝑡 ( 𝑡 ∈ 𝑝 ∧ 𝑢 ∈ 𝑡 ) ) → ∃ 𝑠 ( 𝑠 ∈ 𝑝 ∧ ¬ ∃ 𝑛 𝑛 ∈ 𝑠 ) )
37 ax-1 ⊢ ( 𝑠 ∈ 𝑝 → ( 𝑤 = 𝑦 → 𝑠 ∈ 𝑝 ) )
38 ifpfal ⊢ ( ¬ ∃ 𝑛 𝑛 ∈ 𝑠 → ( if- ( ∃ 𝑛 𝑛 ∈ 𝑠 , 𝑤 = 𝑥 , 𝑤 = 𝑦 ) ↔ 𝑤 = 𝑦 ) )
39 38 biimprd ⊢ ( ¬ ∃ 𝑛 𝑛 ∈ 𝑠 → ( 𝑤 = 𝑦 → if- ( ∃ 𝑛 𝑛 ∈ 𝑠 , 𝑤 = 𝑥 , 𝑤 = 𝑦 ) ) )
40 37 39 anim12ii ⊢ ( ( 𝑠 ∈ 𝑝 ∧ ¬ ∃ 𝑛 𝑛 ∈ 𝑠 ) → ( 𝑤 = 𝑦 → ( 𝑠 ∈ 𝑝 ∧ if- ( ∃ 𝑛 𝑛 ∈ 𝑠 , 𝑤 = 𝑥 , 𝑤 = 𝑦 ) ) ) )
41 40 eximi ⊢ ( ∃ 𝑠 ( 𝑠 ∈ 𝑝 ∧ ¬ ∃ 𝑛 𝑛 ∈ 𝑠 ) → ∃ 𝑠 ( 𝑤 = 𝑦 → ( 𝑠 ∈ 𝑝 ∧ if- ( ∃ 𝑛 𝑛 ∈ 𝑠 , 𝑤 = 𝑥 , 𝑤 = 𝑦 ) ) ) )
42 19.37imv ⊢ ( ∃ 𝑠 ( 𝑤 = 𝑦 → ( 𝑠 ∈ 𝑝 ∧ if- ( ∃ 𝑛 𝑛 ∈ 𝑠 , 𝑤 = 𝑥 , 𝑤 = 𝑦 ) ) ) → ( 𝑤 = 𝑦 → ∃ 𝑠 ( 𝑠 ∈ 𝑝 ∧ if- ( ∃ 𝑛 𝑛 ∈ 𝑠 , 𝑤 = 𝑥 , 𝑤 = 𝑦 ) ) ) )
43 36 41 42 3syl ⊢ ( ∃ 𝑢 ( 𝑢 ∈ 𝑝 ∧ ∀ 𝑡 ¬ 𝑡 ∈ 𝑢 ∧ ∃ 𝑡 ( 𝑡 ∈ 𝑝 ∧ 𝑢 ∈ 𝑡 ) ) → ( 𝑤 = 𝑦 → ∃ 𝑠 ( 𝑠 ∈ 𝑝 ∧ if- ( ∃ 𝑛 𝑛 ∈ 𝑠 , 𝑤 = 𝑥 , 𝑤 = 𝑦 ) ) ) )
44 18 43 jaod ⊢ ( ∃ 𝑢 ( 𝑢 ∈ 𝑝 ∧ ∀ 𝑡 ¬ 𝑡 ∈ 𝑢 ∧ ∃ 𝑡 ( 𝑡 ∈ 𝑝 ∧ 𝑢 ∈ 𝑡 ) ) → ( ( 𝑤 = 𝑥 ∨ 𝑤 = 𝑦 ) → ∃ 𝑠 ( 𝑠 ∈ 𝑝 ∧ if- ( ∃ 𝑛 𝑛 ∈ 𝑠 , 𝑤 = 𝑥 , 𝑤 = 𝑦 ) ) ) )
45 imbi2 ⊢ ( ( 𝑤 ∈ 𝑧 ↔ ∃ 𝑠 ( 𝑠 ∈ 𝑝 ∧ if- ( ∃ 𝑛 𝑛 ∈ 𝑠 , 𝑤 = 𝑥 , 𝑤 = 𝑦 ) ) ) → ( ( ( 𝑤 = 𝑥 ∨ 𝑤 = 𝑦 ) → 𝑤 ∈ 𝑧 ) ↔ ( ( 𝑤 = 𝑥 ∨ 𝑤 = 𝑦 ) → ∃ 𝑠 ( 𝑠 ∈ 𝑝 ∧ if- ( ∃ 𝑛 𝑛 ∈ 𝑠 , 𝑤 = 𝑥 , 𝑤 = 𝑦 ) ) ) ) )
46 44 45 syl5ibrcom ⊢ ( ∃ 𝑢 ( 𝑢 ∈ 𝑝 ∧ ∀ 𝑡 ¬ 𝑡 ∈ 𝑢 ∧ ∃ 𝑡 ( 𝑡 ∈ 𝑝 ∧ 𝑢 ∈ 𝑡 ) ) → ( ( 𝑤 ∈ 𝑧 ↔ ∃ 𝑠 ( 𝑠 ∈ 𝑝 ∧ if- ( ∃ 𝑛 𝑛 ∈ 𝑠 , 𝑤 = 𝑥 , 𝑤 = 𝑦 ) ) ) → ( ( 𝑤 = 𝑥 ∨ 𝑤 = 𝑦 ) → 𝑤 ∈ 𝑧 ) ) )
47 46 alimdv ⊢ ( ∃ 𝑢 ( 𝑢 ∈ 𝑝 ∧ ∀ 𝑡 ¬ 𝑡 ∈ 𝑢 ∧ ∃ 𝑡 ( 𝑡 ∈ 𝑝 ∧ 𝑢 ∈ 𝑡 ) ) → ( ∀ 𝑤 ( 𝑤 ∈ 𝑧 ↔ ∃ 𝑠 ( 𝑠 ∈ 𝑝 ∧ if- ( ∃ 𝑛 𝑛 ∈ 𝑠 , 𝑤 = 𝑥 , 𝑤 = 𝑦 ) ) ) → ∀ 𝑤 ( ( 𝑤 = 𝑥 ∨ 𝑤 = 𝑦 ) → 𝑤 ∈ 𝑧 ) ) )
48 47 eximdv ⊢ ( ∃ 𝑢 ( 𝑢 ∈ 𝑝 ∧ ∀ 𝑡 ¬ 𝑡 ∈ 𝑢 ∧ ∃ 𝑡 ( 𝑡 ∈ 𝑝 ∧ 𝑢 ∈ 𝑡 ) ) → ( ∃ 𝑧 ∀ 𝑤 ( 𝑤 ∈ 𝑧 ↔ ∃ 𝑠 ( 𝑠 ∈ 𝑝 ∧ if- ( ∃ 𝑛 𝑛 ∈ 𝑠 , 𝑤 = 𝑥 , 𝑤 = 𝑦 ) ) ) → ∃ 𝑧 ∀ 𝑤 ( ( 𝑤 = 𝑥 ∨ 𝑤 = 𝑦 ) → 𝑤 ∈ 𝑧 ) ) )
49 1 48 mpi ⊢ ( ∃ 𝑢 ( 𝑢 ∈ 𝑝 ∧ ∀ 𝑡 ¬ 𝑡 ∈ 𝑢 ∧ ∃ 𝑡 ( 𝑡 ∈ 𝑝 ∧ 𝑢 ∈ 𝑡 ) ) → ∃ 𝑧 ∀ 𝑤 ( ( 𝑤 = 𝑥 ∨ 𝑤 = 𝑦 ) → 𝑤 ∈ 𝑧 ) )
50 ax-inf2 ⊢ ∃ 𝑝 ( ∃ 𝑢 ( 𝑢 ∈ 𝑝 ∧ ∀ 𝑡 ¬ 𝑡 ∈ 𝑢 ) ∧ ∀ 𝑢 ( 𝑢 ∈ 𝑝 → ∃ 𝑡 ( 𝑡 ∈ 𝑝 ∧ ∀ 𝑣 ( 𝑣 ∈ 𝑡 ↔ ( 𝑣 ∈ 𝑢 ∨ 𝑣 = 𝑢 ) ) ) ) )
51 df-rex ⊢ ( ∃ 𝑢 ∈ 𝑝 ∀ 𝑡 ¬ 𝑡 ∈ 𝑢 ↔ ∃ 𝑢 ( 𝑢 ∈ 𝑝 ∧ ∀ 𝑡 ¬ 𝑡 ∈ 𝑢 ) )
52 df-ral ⊢ ( ∀ 𝑢 ∈ 𝑝 ∃ 𝑡 ( 𝑡 ∈ 𝑝 ∧ ∀ 𝑣 ( 𝑣 ∈ 𝑡 ↔ ( 𝑣 ∈ 𝑢 ∨ 𝑣 = 𝑢 ) ) ) ↔ ∀ 𝑢 ( 𝑢 ∈ 𝑝 → ∃ 𝑡 ( 𝑡 ∈ 𝑝 ∧ ∀ 𝑣 ( 𝑣 ∈ 𝑡 ↔ ( 𝑣 ∈ 𝑢 ∨ 𝑣 = 𝑢 ) ) ) ) )
53 olc ⊢ ( 𝑣 = 𝑢 → ( 𝑣 ∈ 𝑢 ∨ 𝑣 = 𝑢 ) )
54 biimpr ⊢ ( ( 𝑣 ∈ 𝑡 ↔ ( 𝑣 ∈ 𝑢 ∨ 𝑣 = 𝑢 ) ) → ( ( 𝑣 ∈ 𝑢 ∨ 𝑣 = 𝑢 ) → 𝑣 ∈ 𝑡 ) )
55 53 54 syl5 ⊢ ( ( 𝑣 ∈ 𝑡 ↔ ( 𝑣 ∈ 𝑢 ∨ 𝑣 = 𝑢 ) ) → ( 𝑣 = 𝑢 → 𝑣 ∈ 𝑡 ) )
56 55 alimi ⊢ ( ∀ 𝑣 ( 𝑣 ∈ 𝑡 ↔ ( 𝑣 ∈ 𝑢 ∨ 𝑣 = 𝑢 ) ) → ∀ 𝑣 ( 𝑣 = 𝑢 → 𝑣 ∈ 𝑡 ) )
57 elequ1 ⊢ ( 𝑣 = 𝑢 → ( 𝑣 ∈ 𝑡 ↔ 𝑢 ∈ 𝑡 ) )
58 57 equsalvw ⊢ ( ∀ 𝑣 ( 𝑣 = 𝑢 → 𝑣 ∈ 𝑡 ) ↔ 𝑢 ∈ 𝑡 )
59 56 58 sylib ⊢ ( ∀ 𝑣 ( 𝑣 ∈ 𝑡 ↔ ( 𝑣 ∈ 𝑢 ∨ 𝑣 = 𝑢 ) ) → 𝑢 ∈ 𝑡 )
60 59 anim2i ⊢ ( ( 𝑡 ∈ 𝑝 ∧ ∀ 𝑣 ( 𝑣 ∈ 𝑡 ↔ ( 𝑣 ∈ 𝑢 ∨ 𝑣 = 𝑢 ) ) ) → ( 𝑡 ∈ 𝑝 ∧ 𝑢 ∈ 𝑡 ) )
61 60 eximi ⊢ ( ∃ 𝑡 ( 𝑡 ∈ 𝑝 ∧ ∀ 𝑣 ( 𝑣 ∈ 𝑡 ↔ ( 𝑣 ∈ 𝑢 ∨ 𝑣 = 𝑢 ) ) ) → ∃ 𝑡 ( 𝑡 ∈ 𝑝 ∧ 𝑢 ∈ 𝑡 ) )
62 61 ralimi ⊢ ( ∀ 𝑢 ∈ 𝑝 ∃ 𝑡 ( 𝑡 ∈ 𝑝 ∧ ∀ 𝑣 ( 𝑣 ∈ 𝑡 ↔ ( 𝑣 ∈ 𝑢 ∨ 𝑣 = 𝑢 ) ) ) → ∀ 𝑢 ∈ 𝑝 ∃ 𝑡 ( 𝑡 ∈ 𝑝 ∧ 𝑢 ∈ 𝑡 ) )
63 52 62 sylbir ⊢ ( ∀ 𝑢 ( 𝑢 ∈ 𝑝 → ∃ 𝑡 ( 𝑡 ∈ 𝑝 ∧ ∀ 𝑣 ( 𝑣 ∈ 𝑡 ↔ ( 𝑣 ∈ 𝑢 ∨ 𝑣 = 𝑢 ) ) ) ) → ∀ 𝑢 ∈ 𝑝 ∃ 𝑡 ( 𝑡 ∈ 𝑝 ∧ 𝑢 ∈ 𝑡 ) )
64 63 anim2i ⊢ ( ( ∃ 𝑢 ∈ 𝑝 ∀ 𝑡 ¬ 𝑡 ∈ 𝑢 ∧ ∀ 𝑢 ( 𝑢 ∈ 𝑝 → ∃ 𝑡 ( 𝑡 ∈ 𝑝 ∧ ∀ 𝑣 ( 𝑣 ∈ 𝑡 ↔ ( 𝑣 ∈ 𝑢 ∨ 𝑣 = 𝑢 ) ) ) ) ) → ( ∃ 𝑢 ∈ 𝑝 ∀ 𝑡 ¬ 𝑡 ∈ 𝑢 ∧ ∀ 𝑢 ∈ 𝑝 ∃ 𝑡 ( 𝑡 ∈ 𝑝 ∧ 𝑢 ∈ 𝑡 ) ) )
65 51 64 sylanbr ⊢ ( ( ∃ 𝑢 ( 𝑢 ∈ 𝑝 ∧ ∀ 𝑡 ¬ 𝑡 ∈ 𝑢 ) ∧ ∀ 𝑢 ( 𝑢 ∈ 𝑝 → ∃ 𝑡 ( 𝑡 ∈ 𝑝 ∧ ∀ 𝑣 ( 𝑣 ∈ 𝑡 ↔ ( 𝑣 ∈ 𝑢 ∨ 𝑣 = 𝑢 ) ) ) ) ) → ( ∃ 𝑢 ∈ 𝑝 ∀ 𝑡 ¬ 𝑡 ∈ 𝑢 ∧ ∀ 𝑢 ∈ 𝑝 ∃ 𝑡 ( 𝑡 ∈ 𝑝 ∧ 𝑢 ∈ 𝑡 ) ) )
66 50 65 eximii ⊢ ∃ 𝑝 ( ∃ 𝑢 ∈ 𝑝 ∀ 𝑡 ¬ 𝑡 ∈ 𝑢 ∧ ∀ 𝑢 ∈ 𝑝 ∃ 𝑡 ( 𝑡 ∈ 𝑝 ∧ 𝑢 ∈ 𝑡 ) )
67 r19.29r ⊢ ( ( ∃ 𝑢 ∈ 𝑝 ∀ 𝑡 ¬ 𝑡 ∈ 𝑢 ∧ ∀ 𝑢 ∈ 𝑝 ∃ 𝑡 ( 𝑡 ∈ 𝑝 ∧ 𝑢 ∈ 𝑡 ) ) → ∃ 𝑢 ∈ 𝑝 ( ∀ 𝑡 ¬ 𝑡 ∈ 𝑢 ∧ ∃ 𝑡 ( 𝑡 ∈ 𝑝 ∧ 𝑢 ∈ 𝑡 ) ) )
68 66 67 eximii ⊢ ∃ 𝑝 ∃ 𝑢 ∈ 𝑝 ( ∀ 𝑡 ¬ 𝑡 ∈ 𝑢 ∧ ∃ 𝑡 ( 𝑡 ∈ 𝑝 ∧ 𝑢 ∈ 𝑡 ) )
69 df-rex ⊢ ( ∃ 𝑢 ∈ 𝑝 ( ∀ 𝑡 ¬ 𝑡 ∈ 𝑢 ∧ ∃ 𝑡 ( 𝑡 ∈ 𝑝 ∧ 𝑢 ∈ 𝑡 ) ) ↔ ∃ 𝑢 ( 𝑢 ∈ 𝑝 ∧ ( ∀ 𝑡 ¬ 𝑡 ∈ 𝑢 ∧ ∃ 𝑡 ( 𝑡 ∈ 𝑝 ∧ 𝑢 ∈ 𝑡 ) ) ) )
70 3anass ⊢ ( ( 𝑢 ∈ 𝑝 ∧ ∀ 𝑡 ¬ 𝑡 ∈ 𝑢 ∧ ∃ 𝑡 ( 𝑡 ∈ 𝑝 ∧ 𝑢 ∈ 𝑡 ) ) ↔ ( 𝑢 ∈ 𝑝 ∧ ( ∀ 𝑡 ¬ 𝑡 ∈ 𝑢 ∧ ∃ 𝑡 ( 𝑡 ∈ 𝑝 ∧ 𝑢 ∈ 𝑡 ) ) ) )
71 70 exbii ⊢ ( ∃ 𝑢 ( 𝑢 ∈ 𝑝 ∧ ∀ 𝑡 ¬ 𝑡 ∈ 𝑢 ∧ ∃ 𝑡 ( 𝑡 ∈ 𝑝 ∧ 𝑢 ∈ 𝑡 ) ) ↔ ∃ 𝑢 ( 𝑢 ∈ 𝑝 ∧ ( ∀ 𝑡 ¬ 𝑡 ∈ 𝑢 ∧ ∃ 𝑡 ( 𝑡 ∈ 𝑝 ∧ 𝑢 ∈ 𝑡 ) ) ) )
72 69 71 sylbb2 ⊢ ( ∃ 𝑢 ∈ 𝑝 ( ∀ 𝑡 ¬ 𝑡 ∈ 𝑢 ∧ ∃ 𝑡 ( 𝑡 ∈ 𝑝 ∧ 𝑢 ∈ 𝑡 ) ) → ∃ 𝑢 ( 𝑢 ∈ 𝑝 ∧ ∀ 𝑡 ¬ 𝑡 ∈ 𝑢 ∧ ∃ 𝑡 ( 𝑡 ∈ 𝑝 ∧ 𝑢 ∈ 𝑡 ) ) )
73 68 72 eximii ⊢ ∃ 𝑝 ∃ 𝑢 ( 𝑢 ∈ 𝑝 ∧ ∀ 𝑡 ¬ 𝑡 ∈ 𝑢 ∧ ∃ 𝑡 ( 𝑡 ∈ 𝑝 ∧ 𝑢 ∈ 𝑡 ) )
74 49 73 exlimiiv ⊢ ∃ 𝑧 ∀ 𝑤 ( ( 𝑤 = 𝑥 ∨ 𝑤 = 𝑦 ) → 𝑤 ∈ 𝑧 )