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

Proof

Step Hyp Ref Expression
1 axgroth2 ⊢∃yx∈y∧∀z∈y∀ww⊆z→w∈y∧∃w∈y∀vv⊆z→v∈w∧∀zz⊆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 ⊢∀vv⊆z→v∈w→z⊆z→z∈w
7 2 6 mpi ⊢∀vv⊆z→v∈w→z∈w
8 7 reximi ⊢∃w∈y∀vv⊆z→v∈w→∃w∈yz∈w
9 eluni2 ⊢z∈⋃y↔∃w∈yz∈w
10 8 9 sylibr ⊢∃w∈y∀vv⊆z→v∈w→z∈⋃y
11 10 adantl ⊢∀ww⊆z→w∈y∧∃w∈y∀vv⊆z→v∈w→z∈⋃y
12 11 ralimi ⊢∀z∈y∀ww⊆z→w∈y∧∃w∈y∀vv⊆z→v∈w→∀z∈yz∈⋃y
13 dfss3 ⊢y⊆⋃y↔∀z∈yz∈⋃y
14 12 13 sylibr ⊢∀z∈y∀ww⊆z→w∈y∧∃w∈y∀vv⊆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→∀zz⊆y→y∖z≼z∨z∈y↔∀zz⊆y→y≼z∨z∈y
28 14 27 sylan2 ⊢x∈y∧∀z∈y∀ww⊆z→w∈y∧∃w∈y∀vv⊆z→v∈w→∀zz⊆y→y∖z≼z∨z∈y↔∀zz⊆y→y≼z∨z∈y
29 28 pm5.32i ⊢x∈y∧∀z∈y∀ww⊆z→w∈y∧∃w∈y∀vv⊆z→v∈w∧∀zz⊆y→y∖z≼z∨z∈y↔x∈y∧∀z∈y∀ww⊆z→w∈y∧∃w∈y∀vv⊆z→v∈w∧∀zz⊆y→y≼z∨z∈y
30 df-3an ⊢x∈y∧∀z∈y∀ww⊆z→w∈y∧∃w∈y∀vv⊆z→v∈w∧∀zz⊆y→y∖z≼z∨z∈y↔x∈y∧∀z∈y∀ww⊆z→w∈y∧∃w∈y∀vv⊆z→v∈w∧∀zz⊆y→y∖z≼z∨z∈y
31 df-3an ⊢x∈y∧∀z∈y∀ww⊆z→w∈y∧∃w∈y∀vv⊆z→v∈w∧∀zz⊆y→y≼z∨z∈y↔x∈y∧∀z∈y∀ww⊆z→w∈y∧∃w∈y∀vv⊆z→v∈w∧∀zz⊆y→y≼z∨z∈y
32 29 30 31 3bitr4i ⊢x∈y∧∀z∈y∀ww⊆z→w∈y∧∃w∈y∀vv⊆z→v∈w∧∀zz⊆y→y∖z≼z∨z∈y↔x∈y∧∀z∈y∀ww⊆z→w∈y∧∃w∈y∀vv⊆z→v∈w∧∀zz⊆y→y≼z∨z∈y
33 32 exbii ⊢∃yx∈y∧∀z∈y∀ww⊆z→w∈y∧∃w∈y∀vv⊆z→v∈w∧∀zz⊆y→y∖z≼z∨z∈y↔∃yx∈y∧∀z∈y∀ww⊆z→w∈y∧∃w∈y∀vv⊆z→v∈w∧∀zz⊆y→y≼z∨z∈y
34 1 33 mpbir ⊢∃yx∈y∧∀z∈y∀ww⊆z→w∈y∧∃w∈y∀vv⊆z→v∈w∧∀zz⊆y→y∖z≼z∨z∈y