Metamath Proof Explorer

Theorem axgroth4

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

Ref Expression
Assertion axgroth4 ⊢∃yx∈y∧∀z∈y∃v∈y∀ww⊆z→w∈y∩v∧∀zz⊆y→y∖z≼z∨z∈y

Proof

Step Hyp Ref Expression
1 axgroth3 ⊢∃yx∈y∧∀z∈y∀ww⊆z→w∈y∧∃w∈y∀uu⊆z→u∈w∧∀zz⊆y→y∖z≼z∨z∈y
2 elequ2 ⊢w=v→u∈w↔u∈v
3 2 imbi2d ⊢w=v→u⊆z→u∈w↔u⊆z→u∈v
4 3 albidv ⊢w=v→∀uu⊆z→u∈w↔∀uu⊆z→u∈v
5 4 cbvrexvw ⊢∃w∈y∀uu⊆z→u∈w↔∃v∈y∀uu⊆z→u∈v
6 5 anbi2i ⊢∀ww⊆z→w∈y∧∃w∈y∀uu⊆z→u∈w↔∀ww⊆z→w∈y∧∃v∈y∀uu⊆z→u∈v
7 r19.42v ⊢∃v∈y∀ww⊆z→w∈y∧∀uu⊆z→u∈v↔∀ww⊆z→w∈y∧∃v∈y∀uu⊆z→u∈v
8 sseq1 ⊢u=w→u⊆z↔w⊆z
9 elequ1 ⊢u=w→u∈v↔w∈v
10 8 9 imbi12d ⊢u=w→u⊆z→u∈v↔w⊆z→w∈v
11 10 cbvalvw ⊢∀uu⊆z→u∈v↔∀ww⊆z→w∈v
12 11 anbi2i ⊢∀ww⊆z→w∈y∧∀uu⊆z→u∈v↔∀ww⊆z→w∈y∧∀ww⊆z→w∈v
13 19.26 ⊢∀ww⊆z→w∈y∧w⊆z→w∈v↔∀ww⊆z→w∈y∧∀ww⊆z→w∈v
14 pm4.76 ⊢w⊆z→w∈y∧w⊆z→w∈v↔w⊆z→w∈y∧w∈v
15 elin ⊢w∈y∩v↔w∈y∧w∈v
16 15 imbi2i ⊢w⊆z→w∈y∩v↔w⊆z→w∈y∧w∈v
17 14 16 bitr4i ⊢w⊆z→w∈y∧w⊆z→w∈v↔w⊆z→w∈y∩v
18 17 albii ⊢∀ww⊆z→w∈y∧w⊆z→w∈v↔∀ww⊆z→w∈y∩v
19 12 13 18 3bitr2i ⊢∀ww⊆z→w∈y∧∀uu⊆z→u∈v↔∀ww⊆z→w∈y∩v
20 19 rexbii ⊢∃v∈y∀ww⊆z→w∈y∧∀uu⊆z→u∈v↔∃v∈y∀ww⊆z→w∈y∩v
21 6 7 20 3bitr2i ⊢∀ww⊆z→w∈y∧∃w∈y∀uu⊆z→u∈w↔∃v∈y∀ww⊆z→w∈y∩v
22 21 ralbii ⊢∀z∈y∀ww⊆z→w∈y∧∃w∈y∀uu⊆z→u∈w↔∀z∈y∃v∈y∀ww⊆z→w∈y∩v
23 22 3anbi2i ⊢x∈y∧∀z∈y∀ww⊆z→w∈y∧∃w∈y∀uu⊆z→u∈w∧∀zz⊆y→y∖z≼z∨z∈y↔x∈y∧∀z∈y∃v∈y∀ww⊆z→w∈y∩v∧∀zz⊆y→y∖z≼z∨z∈y
24 23 exbii ⊢∃yx∈y∧∀z∈y∀ww⊆z→w∈y∧∃w∈y∀uu⊆z→u∈w∧∀zz⊆y→y∖z≼z∨z∈y↔∃yx∈y∧∀z∈y∃v∈y∀ww⊆z→w∈y∩v∧∀zz⊆y→y∖z≼z∨z∈y
25 1 24 mpbi ⊢∃yx∈y∧∀z∈y∃v∈y∀ww⊆z→w∈y∩v∧∀zz⊆y→y∖z≼z∨z∈y