Metamath Proof Explorer

Theorem supisoex

Description: Lemma for supiso . (Contributed by Mario Carneiro, 24-Dec-2016)

Ref Expression
Hypotheses supiso.1 ⊢φ→FIsomR,SAB
supiso.2 ⊢φ→C⊆A
supisoex.3 ⊢φ→∃x∈A∀y∈C¬xRy∧∀y∈AyRx→∃z∈CyRz
Assertion supisoex ⊢φ→∃u∈B∀w∈FC¬uSw∧∀w∈BwSu→∃v∈FCwSv

Proof

Step Hyp Ref Expression
1 supiso.1 ⊢φ→FIsomR,SAB
2 supiso.2 ⊢φ→C⊆A
3 supisoex.3 ⊢φ→∃x∈A∀y∈C¬xRy∧∀y∈AyRx→∃z∈CyRz
4 simpl ⊢FIsomR,SAB∧C⊆A→FIsomR,SAB
5 simpr ⊢FIsomR,SAB∧C⊆A→C⊆A
6 4 5 supisolem ⊢FIsomR,SAB∧C⊆A∧x∈A→∀y∈C¬xRy∧∀y∈AyRx→∃z∈CyRz↔∀w∈FC¬F⁡xSw∧∀w∈BwSF⁡x→∃v∈FCwSv
7 isof1o ⊢FIsomR,SAB→F:A⟶1-1 ontoB
8 f1of ⊢F:A⟶1-1 ontoB→F:A⟶B
9 4 7 8 3syl ⊢FIsomR,SAB∧C⊆A→F:A⟶B
10 9 ffvelcdmda ⊢FIsomR,SAB∧C⊆A∧x∈A→F⁡x∈B
11 breq1 ⊢u=F⁡x→uSw↔F⁡xSw
12 11 notbid ⊢u=F⁡x→¬uSw↔¬F⁡xSw
13 12 ralbidv ⊢u=F⁡x→∀w∈FC¬uSw↔∀w∈FC¬F⁡xSw
14 breq2 ⊢u=F⁡x→wSu↔wSF⁡x
15 14 imbi1d ⊢u=F⁡x→wSu→∃v∈FCwSv↔wSF⁡x→∃v∈FCwSv
16 15 ralbidv ⊢u=F⁡x→∀w∈BwSu→∃v∈FCwSv↔∀w∈BwSF⁡x→∃v∈FCwSv
17 13 16 anbi12d ⊢u=F⁡x→∀w∈FC¬uSw∧∀w∈BwSu→∃v∈FCwSv↔∀w∈FC¬F⁡xSw∧∀w∈BwSF⁡x→∃v∈FCwSv
18 17 rspcev ⊢F⁡x∈B∧∀w∈FC¬F⁡xSw∧∀w∈BwSF⁡x→∃v∈FCwSv→∃u∈B∀w∈FC¬uSw∧∀w∈BwSu→∃v∈FCwSv
19 18 ex ⊢F⁡x∈B→∀w∈FC¬F⁡xSw∧∀w∈BwSF⁡x→∃v∈FCwSv→∃u∈B∀w∈FC¬uSw∧∀w∈BwSu→∃v∈FCwSv
20 10 19 syl ⊢FIsomR,SAB∧C⊆A∧x∈A→∀w∈FC¬F⁡xSw∧∀w∈BwSF⁡x→∃v∈FCwSv→∃u∈B∀w∈FC¬uSw∧∀w∈BwSu→∃v∈FCwSv
21 6 20 sylbid ⊢FIsomR,SAB∧C⊆A∧x∈A→∀y∈C¬xRy∧∀y∈AyRx→∃z∈CyRz→∃u∈B∀w∈FC¬uSw∧∀w∈BwSu→∃v∈FCwSv
22 21 rexlimdva ⊢FIsomR,SAB∧C⊆A→∃x∈A∀y∈C¬xRy∧∀y∈AyRx→∃z∈CyRz→∃u∈B∀w∈FC¬uSw∧∀w∈BwSu→∃v∈FCwSv
23 1 2 22 syl2anc ⊢φ→∃x∈A∀y∈C¬xRy∧∀y∈AyRx→∃z∈CyRz→∃u∈B∀w∈FC¬uSw∧∀w∈BwSu→∃v∈FCwSv
24 3 23 mpd ⊢φ→∃u∈B∀w∈FC¬uSw∧∀w∈BwSu→∃v∈FCwSv