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 ⊢ ∃ y x ∈ y ∧ ∀ z ∈ y ∀ w w ⊆ z → w ∈ y ∧ ∃ w ∈ y ∀ v v ⊆ z → v ∈ w ∧ ∀ z z ⊆ y → y ∖ z ≼ z ∨ z ∈ y

Proof

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