# 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 ${⊢}\exists {y}\phantom{\rule{.4em}{0ex}}\left({x}\in {y}\wedge \forall {z}\in {y}\phantom{\rule{.4em}{0ex}}\exists {v}\in {y}\phantom{\rule{.4em}{0ex}}\forall {w}\phantom{\rule{.4em}{0ex}}\left({w}\subseteq {z}\to {w}\in \left({y}\cap {v}\right)\right)\wedge \forall {z}\phantom{\rule{.4em}{0ex}}\left({z}\subseteq {y}\to \left(\left({y}\setminus {z}\right)\preccurlyeq {z}\vee {z}\in {y}\right)\right)\right)$

### Proof

Step Hyp Ref Expression
1 axgroth3 ${⊢}\exists {y}\phantom{\rule{.4em}{0ex}}\left({x}\in {y}\wedge \forall {z}\in {y}\phantom{\rule{.4em}{0ex}}\left(\forall {w}\phantom{\rule{.4em}{0ex}}\left({w}\subseteq {z}\to {w}\in {y}\right)\wedge \exists {w}\in {y}\phantom{\rule{.4em}{0ex}}\forall {u}\phantom{\rule{.4em}{0ex}}\left({u}\subseteq {z}\to {u}\in {w}\right)\right)\wedge \forall {z}\phantom{\rule{.4em}{0ex}}\left({z}\subseteq {y}\to \left(\left({y}\setminus {z}\right)\preccurlyeq {z}\vee {z}\in {y}\right)\right)\right)$
2 elequ2 ${⊢}{w}={v}\to \left({u}\in {w}↔{u}\in {v}\right)$
3 2 imbi2d ${⊢}{w}={v}\to \left(\left({u}\subseteq {z}\to {u}\in {w}\right)↔\left({u}\subseteq {z}\to {u}\in {v}\right)\right)$
4 3 albidv ${⊢}{w}={v}\to \left(\forall {u}\phantom{\rule{.4em}{0ex}}\left({u}\subseteq {z}\to {u}\in {w}\right)↔\forall {u}\phantom{\rule{.4em}{0ex}}\left({u}\subseteq {z}\to {u}\in {v}\right)\right)$
5 4 cbvrexvw ${⊢}\exists {w}\in {y}\phantom{\rule{.4em}{0ex}}\forall {u}\phantom{\rule{.4em}{0ex}}\left({u}\subseteq {z}\to {u}\in {w}\right)↔\exists {v}\in {y}\phantom{\rule{.4em}{0ex}}\forall {u}\phantom{\rule{.4em}{0ex}}\left({u}\subseteq {z}\to {u}\in {v}\right)$
6 5 anbi2i ${⊢}\left(\forall {w}\phantom{\rule{.4em}{0ex}}\left({w}\subseteq {z}\to {w}\in {y}\right)\wedge \exists {w}\in {y}\phantom{\rule{.4em}{0ex}}\forall {u}\phantom{\rule{.4em}{0ex}}\left({u}\subseteq {z}\to {u}\in {w}\right)\right)↔\left(\forall {w}\phantom{\rule{.4em}{0ex}}\left({w}\subseteq {z}\to {w}\in {y}\right)\wedge \exists {v}\in {y}\phantom{\rule{.4em}{0ex}}\forall {u}\phantom{\rule{.4em}{0ex}}\left({u}\subseteq {z}\to {u}\in {v}\right)\right)$
7 r19.42v ${⊢}\exists {v}\in {y}\phantom{\rule{.4em}{0ex}}\left(\forall {w}\phantom{\rule{.4em}{0ex}}\left({w}\subseteq {z}\to {w}\in {y}\right)\wedge \forall {u}\phantom{\rule{.4em}{0ex}}\left({u}\subseteq {z}\to {u}\in {v}\right)\right)↔\left(\forall {w}\phantom{\rule{.4em}{0ex}}\left({w}\subseteq {z}\to {w}\in {y}\right)\wedge \exists {v}\in {y}\phantom{\rule{.4em}{0ex}}\forall {u}\phantom{\rule{.4em}{0ex}}\left({u}\subseteq {z}\to {u}\in {v}\right)\right)$
8 sseq1 ${⊢}{u}={w}\to \left({u}\subseteq {z}↔{w}\subseteq {z}\right)$
9 elequ1 ${⊢}{u}={w}\to \left({u}\in {v}↔{w}\in {v}\right)$
10 8 9 imbi12d ${⊢}{u}={w}\to \left(\left({u}\subseteq {z}\to {u}\in {v}\right)↔\left({w}\subseteq {z}\to {w}\in {v}\right)\right)$
11 10 cbvalvw ${⊢}\forall {u}\phantom{\rule{.4em}{0ex}}\left({u}\subseteq {z}\to {u}\in {v}\right)↔\forall {w}\phantom{\rule{.4em}{0ex}}\left({w}\subseteq {z}\to {w}\in {v}\right)$
12 11 anbi2i ${⊢}\left(\forall {w}\phantom{\rule{.4em}{0ex}}\left({w}\subseteq {z}\to {w}\in {y}\right)\wedge \forall {u}\phantom{\rule{.4em}{0ex}}\left({u}\subseteq {z}\to {u}\in {v}\right)\right)↔\left(\forall {w}\phantom{\rule{.4em}{0ex}}\left({w}\subseteq {z}\to {w}\in {y}\right)\wedge \forall {w}\phantom{\rule{.4em}{0ex}}\left({w}\subseteq {z}\to {w}\in {v}\right)\right)$
13 19.26 ${⊢}\forall {w}\phantom{\rule{.4em}{0ex}}\left(\left({w}\subseteq {z}\to {w}\in {y}\right)\wedge \left({w}\subseteq {z}\to {w}\in {v}\right)\right)↔\left(\forall {w}\phantom{\rule{.4em}{0ex}}\left({w}\subseteq {z}\to {w}\in {y}\right)\wedge \forall {w}\phantom{\rule{.4em}{0ex}}\left({w}\subseteq {z}\to {w}\in {v}\right)\right)$
14 pm4.76 ${⊢}\left(\left({w}\subseteq {z}\to {w}\in {y}\right)\wedge \left({w}\subseteq {z}\to {w}\in {v}\right)\right)↔\left({w}\subseteq {z}\to \left({w}\in {y}\wedge {w}\in {v}\right)\right)$
15 elin ${⊢}{w}\in \left({y}\cap {v}\right)↔\left({w}\in {y}\wedge {w}\in {v}\right)$
16 15 imbi2i ${⊢}\left({w}\subseteq {z}\to {w}\in \left({y}\cap {v}\right)\right)↔\left({w}\subseteq {z}\to \left({w}\in {y}\wedge {w}\in {v}\right)\right)$
17 14 16 bitr4i ${⊢}\left(\left({w}\subseteq {z}\to {w}\in {y}\right)\wedge \left({w}\subseteq {z}\to {w}\in {v}\right)\right)↔\left({w}\subseteq {z}\to {w}\in \left({y}\cap {v}\right)\right)$
18 17 albii ${⊢}\forall {w}\phantom{\rule{.4em}{0ex}}\left(\left({w}\subseteq {z}\to {w}\in {y}\right)\wedge \left({w}\subseteq {z}\to {w}\in {v}\right)\right)↔\forall {w}\phantom{\rule{.4em}{0ex}}\left({w}\subseteq {z}\to {w}\in \left({y}\cap {v}\right)\right)$
19 12 13 18 3bitr2i ${⊢}\left(\forall {w}\phantom{\rule{.4em}{0ex}}\left({w}\subseteq {z}\to {w}\in {y}\right)\wedge \forall {u}\phantom{\rule{.4em}{0ex}}\left({u}\subseteq {z}\to {u}\in {v}\right)\right)↔\forall {w}\phantom{\rule{.4em}{0ex}}\left({w}\subseteq {z}\to {w}\in \left({y}\cap {v}\right)\right)$
20 19 rexbii ${⊢}\exists {v}\in {y}\phantom{\rule{.4em}{0ex}}\left(\forall {w}\phantom{\rule{.4em}{0ex}}\left({w}\subseteq {z}\to {w}\in {y}\right)\wedge \forall {u}\phantom{\rule{.4em}{0ex}}\left({u}\subseteq {z}\to {u}\in {v}\right)\right)↔\exists {v}\in {y}\phantom{\rule{.4em}{0ex}}\forall {w}\phantom{\rule{.4em}{0ex}}\left({w}\subseteq {z}\to {w}\in \left({y}\cap {v}\right)\right)$
21 6 7 20 3bitr2i ${⊢}\left(\forall {w}\phantom{\rule{.4em}{0ex}}\left({w}\subseteq {z}\to {w}\in {y}\right)\wedge \exists {w}\in {y}\phantom{\rule{.4em}{0ex}}\forall {u}\phantom{\rule{.4em}{0ex}}\left({u}\subseteq {z}\to {u}\in {w}\right)\right)↔\exists {v}\in {y}\phantom{\rule{.4em}{0ex}}\forall {w}\phantom{\rule{.4em}{0ex}}\left({w}\subseteq {z}\to {w}\in \left({y}\cap {v}\right)\right)$
22 21 ralbii ${⊢}\forall {z}\in {y}\phantom{\rule{.4em}{0ex}}\left(\forall {w}\phantom{\rule{.4em}{0ex}}\left({w}\subseteq {z}\to {w}\in {y}\right)\wedge \exists {w}\in {y}\phantom{\rule{.4em}{0ex}}\forall {u}\phantom{\rule{.4em}{0ex}}\left({u}\subseteq {z}\to {u}\in {w}\right)\right)↔\forall {z}\in {y}\phantom{\rule{.4em}{0ex}}\exists {v}\in {y}\phantom{\rule{.4em}{0ex}}\forall {w}\phantom{\rule{.4em}{0ex}}\left({w}\subseteq {z}\to {w}\in \left({y}\cap {v}\right)\right)$
23 22 3anbi2i ${⊢}\left({x}\in {y}\wedge \forall {z}\in {y}\phantom{\rule{.4em}{0ex}}\left(\forall {w}\phantom{\rule{.4em}{0ex}}\left({w}\subseteq {z}\to {w}\in {y}\right)\wedge \exists {w}\in {y}\phantom{\rule{.4em}{0ex}}\forall {u}\phantom{\rule{.4em}{0ex}}\left({u}\subseteq {z}\to {u}\in {w}\right)\right)\wedge \forall {z}\phantom{\rule{.4em}{0ex}}\left({z}\subseteq {y}\to \left(\left({y}\setminus {z}\right)\preccurlyeq {z}\vee {z}\in {y}\right)\right)\right)↔\left({x}\in {y}\wedge \forall {z}\in {y}\phantom{\rule{.4em}{0ex}}\exists {v}\in {y}\phantom{\rule{.4em}{0ex}}\forall {w}\phantom{\rule{.4em}{0ex}}\left({w}\subseteq {z}\to {w}\in \left({y}\cap {v}\right)\right)\wedge \forall {z}\phantom{\rule{.4em}{0ex}}\left({z}\subseteq {y}\to \left(\left({y}\setminus {z}\right)\preccurlyeq {z}\vee {z}\in {y}\right)\right)\right)$
24 23 exbii ${⊢}\exists {y}\phantom{\rule{.4em}{0ex}}\left({x}\in {y}\wedge \forall {z}\in {y}\phantom{\rule{.4em}{0ex}}\left(\forall {w}\phantom{\rule{.4em}{0ex}}\left({w}\subseteq {z}\to {w}\in {y}\right)\wedge \exists {w}\in {y}\phantom{\rule{.4em}{0ex}}\forall {u}\phantom{\rule{.4em}{0ex}}\left({u}\subseteq {z}\to {u}\in {w}\right)\right)\wedge \forall {z}\phantom{\rule{.4em}{0ex}}\left({z}\subseteq {y}\to \left(\left({y}\setminus {z}\right)\preccurlyeq {z}\vee {z}\in {y}\right)\right)\right)↔\exists {y}\phantom{\rule{.4em}{0ex}}\left({x}\in {y}\wedge \forall {z}\in {y}\phantom{\rule{.4em}{0ex}}\exists {v}\in {y}\phantom{\rule{.4em}{0ex}}\forall {w}\phantom{\rule{.4em}{0ex}}\left({w}\subseteq {z}\to {w}\in \left({y}\cap {v}\right)\right)\wedge \forall {z}\phantom{\rule{.4em}{0ex}}\left({z}\subseteq {y}\to \left(\left({y}\setminus {z}\right)\preccurlyeq {z}\vee {z}\in {y}\right)\right)\right)$
25 1 24 mpbi ${⊢}\exists {y}\phantom{\rule{.4em}{0ex}}\left({x}\in {y}\wedge \forall {z}\in {y}\phantom{\rule{.4em}{0ex}}\exists {v}\in {y}\phantom{\rule{.4em}{0ex}}\forall {w}\phantom{\rule{.4em}{0ex}}\left({w}\subseteq {z}\to {w}\in \left({y}\cap {v}\right)\right)\wedge \forall {z}\phantom{\rule{.4em}{0ex}}\left({z}\subseteq {y}\to \left(\left({y}\setminus {z}\right)\preccurlyeq {z}\vee {z}\in {y}\right)\right)\right)$