Metamath Proof Explorer

Theorem axgroth3

Description: Alternate version of the Tarski-Grothendieck Axiom. ax-cc is used to derive this version. (Contributed by NM, 26-Mar-2007)

Ref Expression
Assertion axgroth3 ∃ 𝑦 ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑧 ∈ 𝑦 ( ∀ 𝑤 ( 𝑤 ⊆ 𝑧 → 𝑤 ∈ 𝑦 ) ∧ ∃ 𝑤 ∈ 𝑦 ∀ 𝑣 ( 𝑣 ⊆ 𝑧 → 𝑣 ∈ 𝑤 ) ) ∧ ∀ 𝑧 ( 𝑧 ⊆ 𝑦 → ( ( 𝑦 ∖ 𝑧 ) ≼ 𝑧 ∨ 𝑧 ∈ 𝑦 ) ) )

Proof

Step Hyp Ref Expression
1 axgroth2 ⊢ ∃ 𝑦 ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑧 ∈ 𝑦 ( ∀ 𝑤 ( 𝑤 ⊆ 𝑧 → 𝑤 ∈ 𝑦 ) ∧ ∃ 𝑤 ∈ 𝑦 ∀ 𝑣 ( 𝑣 ⊆ 𝑧 → 𝑣 ∈ 𝑤 ) ) ∧ ∀ 𝑧 ( 𝑧 ⊆ 𝑦 → ( 𝑦 ≼ 𝑧 ∨ 𝑧 ∈ 𝑦 ) ) )
2 ssid ⊢ 𝑧 ⊆ 𝑧
3 sseq1 ⊢ ( 𝑣 = 𝑧 → ( 𝑣 ⊆ 𝑧 ↔ 𝑧 ⊆ 𝑧 ) )
4 elequ1 ⊢ ( 𝑣 = 𝑧 → ( 𝑣 ∈ 𝑤 ↔ 𝑧 ∈ 𝑤 ) )
5 3 4 imbi12d ⊢ ( 𝑣 = 𝑧 → ( ( 𝑣 ⊆ 𝑧 → 𝑣 ∈ 𝑤 ) ↔ ( 𝑧 ⊆ 𝑧 → 𝑧 ∈ 𝑤 ) ) )
6 5 spvv ⊢ ( ∀ 𝑣 ( 𝑣 ⊆ 𝑧 → 𝑣 ∈ 𝑤 ) → ( 𝑧 ⊆ 𝑧 → 𝑧 ∈ 𝑤 ) )
7 2 6 mpi ⊢ ( ∀ 𝑣 ( 𝑣 ⊆ 𝑧 → 𝑣 ∈ 𝑤 ) → 𝑧 ∈ 𝑤 )
8 7 reximi ⊢ ( ∃ 𝑤 ∈ 𝑦 ∀ 𝑣 ( 𝑣 ⊆ 𝑧 → 𝑣 ∈ 𝑤 ) → ∃ 𝑤 ∈ 𝑦 𝑧 ∈ 𝑤 )
9 eluni2 ⊢ ( 𝑧 ∈ ∪ 𝑦 ↔ ∃ 𝑤 ∈ 𝑦 𝑧 ∈ 𝑤 )
10 8 9 sylibr ⊢ ( ∃ 𝑤 ∈ 𝑦 ∀ 𝑣 ( 𝑣 ⊆ 𝑧 → 𝑣 ∈ 𝑤 ) → 𝑧 ∈ ∪ 𝑦 )
11 10 adantl ⊢ ( ( ∀ 𝑤 ( 𝑤 ⊆ 𝑧 → 𝑤 ∈ 𝑦 ) ∧ ∃ 𝑤 ∈ 𝑦 ∀ 𝑣 ( 𝑣 ⊆ 𝑧 → 𝑣 ∈ 𝑤 ) ) → 𝑧 ∈ ∪ 𝑦 )
12 11 ralimi ⊢ ( ∀ 𝑧 ∈ 𝑦 ( ∀ 𝑤 ( 𝑤 ⊆ 𝑧 → 𝑤 ∈ 𝑦 ) ∧ ∃ 𝑤 ∈ 𝑦 ∀ 𝑣 ( 𝑣 ⊆ 𝑧 → 𝑣 ∈ 𝑤 ) ) → ∀ 𝑧 ∈ 𝑦 𝑧 ∈ ∪ 𝑦 )
13 dfss3 ⊢ ( 𝑦 ⊆ ∪ 𝑦 ↔ ∀ 𝑧 ∈ 𝑦 𝑧 ∈ ∪ 𝑦 )
14 12 13 sylibr ⊢ ( ∀ 𝑧 ∈ 𝑦 ( ∀ 𝑤 ( 𝑤 ⊆ 𝑧 → 𝑤 ∈ 𝑦 ) ∧ ∃ 𝑤 ∈ 𝑦 ∀ 𝑣 ( 𝑣 ⊆ 𝑧 → 𝑣 ∈ 𝑤 ) ) → 𝑦 ⊆ ∪ 𝑦 )
15 vex ⊢ 𝑦 ∈ V
16 grothac ⊢ dom card = V
17 15 16 eleqtrri ⊢ 𝑦 ∈ dom card
18 vex ⊢ 𝑧 ∈ V
19 18 16 eleqtrri ⊢ 𝑧 ∈ dom card
20 ne0i ⊢ ( 𝑥 ∈ 𝑦 → 𝑦 ≠ ∅ )
21 15 dominf ⊢ ( ( 𝑦 ≠ ∅ ∧ 𝑦 ⊆ ∪ 𝑦 ) → ω ≼ 𝑦 )
22 20 21 sylan ⊢ ( ( 𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ ∪ 𝑦 ) → ω ≼ 𝑦 )
23 infdif2 ⊢ ( ( 𝑦 ∈ dom card ∧ 𝑧 ∈ dom card ∧ ω ≼ 𝑦 ) → ( ( 𝑦 ∖ 𝑧 ) ≼ 𝑧 ↔ 𝑦 ≼ 𝑧 ) )
24 17 19 22 23 mp3an12i ⊢ ( ( 𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ ∪ 𝑦 ) → ( ( 𝑦 ∖ 𝑧 ) ≼ 𝑧 ↔ 𝑦 ≼ 𝑧 ) )
25 24 orbi1d ⊢ ( ( 𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ ∪ 𝑦 ) → ( ( ( 𝑦 ∖ 𝑧 ) ≼ 𝑧 ∨ 𝑧 ∈ 𝑦 ) ↔ ( 𝑦 ≼ 𝑧 ∨ 𝑧 ∈ 𝑦 ) ) )
26 25 imbi2d ⊢ ( ( 𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ ∪ 𝑦 ) → ( ( 𝑧 ⊆ 𝑦 → ( ( 𝑦 ∖ 𝑧 ) ≼ 𝑧 ∨ 𝑧 ∈ 𝑦 ) ) ↔ ( 𝑧 ⊆ 𝑦 → ( 𝑦 ≼ 𝑧 ∨ 𝑧 ∈ 𝑦 ) ) ) )
27 26 albidv ⊢ ( ( 𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ ∪ 𝑦 ) → ( ∀ 𝑧 ( 𝑧 ⊆ 𝑦 → ( ( 𝑦 ∖ 𝑧 ) ≼ 𝑧 ∨ 𝑧 ∈ 𝑦 ) ) ↔ ∀ 𝑧 ( 𝑧 ⊆ 𝑦 → ( 𝑦 ≼ 𝑧 ∨ 𝑧 ∈ 𝑦 ) ) ) )
28 14 27 sylan2 ⊢ ( ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑧 ∈ 𝑦 ( ∀ 𝑤 ( 𝑤 ⊆ 𝑧 → 𝑤 ∈ 𝑦 ) ∧ ∃ 𝑤 ∈ 𝑦 ∀ 𝑣 ( 𝑣 ⊆ 𝑧 → 𝑣 ∈ 𝑤 ) ) ) → ( ∀ 𝑧 ( 𝑧 ⊆ 𝑦 → ( ( 𝑦 ∖ 𝑧 ) ≼ 𝑧 ∨ 𝑧 ∈ 𝑦 ) ) ↔ ∀ 𝑧 ( 𝑧 ⊆ 𝑦 → ( 𝑦 ≼ 𝑧 ∨ 𝑧 ∈ 𝑦 ) ) ) )
29 28 pm5.32i ⊢ ( ( ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑧 ∈ 𝑦 ( ∀ 𝑤 ( 𝑤 ⊆ 𝑧 → 𝑤 ∈ 𝑦 ) ∧ ∃ 𝑤 ∈ 𝑦 ∀ 𝑣 ( 𝑣 ⊆ 𝑧 → 𝑣 ∈ 𝑤 ) ) ) ∧ ∀ 𝑧 ( 𝑧 ⊆ 𝑦 → ( ( 𝑦 ∖ 𝑧 ) ≼ 𝑧 ∨ 𝑧 ∈ 𝑦 ) ) ) ↔ ( ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑧 ∈ 𝑦 ( ∀ 𝑤 ( 𝑤 ⊆ 𝑧 → 𝑤 ∈ 𝑦 ) ∧ ∃ 𝑤 ∈ 𝑦 ∀ 𝑣 ( 𝑣 ⊆ 𝑧 → 𝑣 ∈ 𝑤 ) ) ) ∧ ∀ 𝑧 ( 𝑧 ⊆ 𝑦 → ( 𝑦 ≼ 𝑧 ∨ 𝑧 ∈ 𝑦 ) ) ) )
30 df-3an ⊢ ( ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑧 ∈ 𝑦 ( ∀ 𝑤 ( 𝑤 ⊆ 𝑧 → 𝑤 ∈ 𝑦 ) ∧ ∃ 𝑤 ∈ 𝑦 ∀ 𝑣 ( 𝑣 ⊆ 𝑧 → 𝑣 ∈ 𝑤 ) ) ∧ ∀ 𝑧 ( 𝑧 ⊆ 𝑦 → ( ( 𝑦 ∖ 𝑧 ) ≼ 𝑧 ∨ 𝑧 ∈ 𝑦 ) ) ) ↔ ( ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑧 ∈ 𝑦 ( ∀ 𝑤 ( 𝑤 ⊆ 𝑧 → 𝑤 ∈ 𝑦 ) ∧ ∃ 𝑤 ∈ 𝑦 ∀ 𝑣 ( 𝑣 ⊆ 𝑧 → 𝑣 ∈ 𝑤 ) ) ) ∧ ∀ 𝑧 ( 𝑧 ⊆ 𝑦 → ( ( 𝑦 ∖ 𝑧 ) ≼ 𝑧 ∨ 𝑧 ∈ 𝑦 ) ) ) )
31 df-3an ⊢ ( ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑧 ∈ 𝑦 ( ∀ 𝑤 ( 𝑤 ⊆ 𝑧 → 𝑤 ∈ 𝑦 ) ∧ ∃ 𝑤 ∈ 𝑦 ∀ 𝑣 ( 𝑣 ⊆ 𝑧 → 𝑣 ∈ 𝑤 ) ) ∧ ∀ 𝑧 ( 𝑧 ⊆ 𝑦 → ( 𝑦 ≼ 𝑧 ∨ 𝑧 ∈ 𝑦 ) ) ) ↔ ( ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑧 ∈ 𝑦 ( ∀ 𝑤 ( 𝑤 ⊆ 𝑧 → 𝑤 ∈ 𝑦 ) ∧ ∃ 𝑤 ∈ 𝑦 ∀ 𝑣 ( 𝑣 ⊆ 𝑧 → 𝑣 ∈ 𝑤 ) ) ) ∧ ∀ 𝑧 ( 𝑧 ⊆ 𝑦 → ( 𝑦 ≼ 𝑧 ∨ 𝑧 ∈ 𝑦 ) ) ) )
32 29 30 31 3bitr4i ⊢ ( ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑧 ∈ 𝑦 ( ∀ 𝑤 ( 𝑤 ⊆ 𝑧 → 𝑤 ∈ 𝑦 ) ∧ ∃ 𝑤 ∈ 𝑦 ∀ 𝑣 ( 𝑣 ⊆ 𝑧 → 𝑣 ∈ 𝑤 ) ) ∧ ∀ 𝑧 ( 𝑧 ⊆ 𝑦 → ( ( 𝑦 ∖ 𝑧 ) ≼ 𝑧 ∨ 𝑧 ∈ 𝑦 ) ) ) ↔ ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑧 ∈ 𝑦 ( ∀ 𝑤 ( 𝑤 ⊆ 𝑧 → 𝑤 ∈ 𝑦 ) ∧ ∃ 𝑤 ∈ 𝑦 ∀ 𝑣 ( 𝑣 ⊆ 𝑧 → 𝑣 ∈ 𝑤 ) ) ∧ ∀ 𝑧 ( 𝑧 ⊆ 𝑦 → ( 𝑦 ≼ 𝑧 ∨ 𝑧 ∈ 𝑦 ) ) ) )
33 32 exbii ⊢ ( ∃ 𝑦 ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑧 ∈ 𝑦 ( ∀ 𝑤 ( 𝑤 ⊆ 𝑧 → 𝑤 ∈ 𝑦 ) ∧ ∃ 𝑤 ∈ 𝑦 ∀ 𝑣 ( 𝑣 ⊆ 𝑧 → 𝑣 ∈ 𝑤 ) ) ∧ ∀ 𝑧 ( 𝑧 ⊆ 𝑦 → ( ( 𝑦 ∖ 𝑧 ) ≼ 𝑧 ∨ 𝑧 ∈ 𝑦 ) ) ) ↔ ∃ 𝑦 ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑧 ∈ 𝑦 ( ∀ 𝑤 ( 𝑤 ⊆ 𝑧 → 𝑤 ∈ 𝑦 ) ∧ ∃ 𝑤 ∈ 𝑦 ∀ 𝑣 ( 𝑣 ⊆ 𝑧 → 𝑣 ∈ 𝑤 ) ) ∧ ∀ 𝑧 ( 𝑧 ⊆ 𝑦 → ( 𝑦 ≼ 𝑧 ∨ 𝑧 ∈ 𝑦 ) ) ) )
34 1 33 mpbir ⊢ ∃ 𝑦 ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑧 ∈ 𝑦 ( ∀ 𝑤 ( 𝑤 ⊆ 𝑧 → 𝑤 ∈ 𝑦 ) ∧ ∃ 𝑤 ∈ 𝑦 ∀ 𝑣 ( 𝑣 ⊆ 𝑧 → 𝑣 ∈ 𝑤 ) ) ∧ ∀ 𝑧 ( 𝑧 ⊆ 𝑦 → ( ( 𝑦 ∖ 𝑧 ) ≼ 𝑧 ∨ 𝑧 ∈ 𝑦 ) ) )