supisolem

	Ref	Expression
Hypotheses	supiso.1	$⊢ φ \to F {Isom}_{R, S} (A, B)$
	supiso.2	$⊢ φ \to C \subseteq A$
Assertion	supisolem	$⊢ (φ \land D \in A) \to ((\forall y \in C \neg D R y \land \forall y \in A (y R D \to \exists z \in C y R z)) \leftrightarrow (\forall w \in F [C] \neg F (D) S w \land \forall w \in B (w S F (D) \to \exists v \in F [C] w S v)))$

Proof

Step	Hyp	Ref	Expression
1		supiso.1	$⊢ φ \to F {Isom}_{R, S} (A, B)$
2		supiso.2	$⊢ φ \to C \subseteq A$
3	1 2	jca	$⊢ φ \to (F {Isom}_{R, S} (A, B) \land C \subseteq A)$
4		simpll	$⊢ ((F {Isom}_{R, S} (A, B) \land C \subseteq A) \land D \in A) \to F {Isom}_{R, S} (A, B)$
5	4	adantr	$⊢ (((F {Isom}_{R, S} (A, B) \land C \subseteq A) \land D \in A) \land y \in C) \to F {Isom}_{R, S} (A, B)$
6		simplr	$⊢ (((F {Isom}_{R, S} (A, B) \land C \subseteq A) \land D \in A) \land y \in C) \to D \in A$
7		simplr	$⊢ ((F {Isom}_{R, S} (A, B) \land C \subseteq A) \land D \in A) \to C \subseteq A$
8	7	sselda	$⊢ (((F {Isom}_{R, S} (A, B) \land C \subseteq A) \land D \in A) \land y \in C) \to y \in A$
9		isorel	$⊢ (F {Isom}_{R, S} (A, B) \land (D \in A \land y \in A)) \to (D R y \leftrightarrow F (D) S F (y))$
10	5 6 8 9	syl12anc	$⊢ (((F {Isom}_{R, S} (A, B) \land C \subseteq A) \land D \in A) \land y \in C) \to (D R y \leftrightarrow F (D) S F (y))$
11	10	notbid	$⊢ (((F {Isom}_{R, S} (A, B) \land C \subseteq A) \land D \in A) \land y \in C) \to (\neg D R y \leftrightarrow \neg F (D) S F (y))$
12	11	ralbidva	$⊢ ((F {Isom}_{R, S} (A, B) \land C \subseteq A) \land D \in A) \to (\forall y \in C \neg D R y \leftrightarrow \forall y \in C \neg F (D) S F (y))$
13		isof1o	$⊢ F {Isom}_{R, S} (A, B) \to F : A \underset{1-1 onto}{⟶} B$
14	4 13	syl	$⊢ ((F {Isom}_{R, S} (A, B) \land C \subseteq A) \land D \in A) \to F : A \underset{1-1 onto}{⟶} B$
15		f1ofn	$⊢ F : A \underset{1-1 onto}{⟶} B \to F Fn A$
16	14 15	syl	$⊢ ((F {Isom}_{R, S} (A, B) \land C \subseteq A) \land D \in A) \to F Fn A$
17		breq2	$⊢ w = F (y) \to (F (D) S w \leftrightarrow F (D) S F (y))$
18	17	notbid	$⊢ w = F (y) \to (\neg F (D) S w \leftrightarrow \neg F (D) S F (y))$
19	18	ralima	$⊢ (F Fn A \land C \subseteq A) \to (\forall w \in F [C] \neg F (D) S w \leftrightarrow \forall y \in C \neg F (D) S F (y))$
20	16 7 19	syl2anc	$⊢ ((F {Isom}_{R, S} (A, B) \land C \subseteq A) \land D \in A) \to (\forall w \in F [C] \neg F (D) S w \leftrightarrow \forall y \in C \neg F (D) S F (y))$
21	12 20	bitr4d	$⊢ ((F {Isom}_{R, S} (A, B) \land C \subseteq A) \land D \in A) \to (\forall y \in C \neg D R y \leftrightarrow \forall w \in F [C] \neg F (D) S w)$
22	4	adantr	$⊢ (((F {Isom}_{R, S} (A, B) \land C \subseteq A) \land D \in A) \land y \in A) \to F {Isom}_{R, S} (A, B)$
23		simpr	$⊢ (((F {Isom}_{R, S} (A, B) \land C \subseteq A) \land D \in A) \land y \in A) \to y \in A$
24		simplr	$⊢ (((F {Isom}_{R, S} (A, B) \land C \subseteq A) \land D \in A) \land y \in A) \to D \in A$
25		isorel	$⊢ (F {Isom}_{R, S} (A, B) \land (y \in A \land D \in A)) \to (y R D \leftrightarrow F (y) S F (D))$
26	22 23 24 25	syl12anc	$⊢ (((F {Isom}_{R, S} (A, B) \land C \subseteq A) \land D \in A) \land y \in A) \to (y R D \leftrightarrow F (y) S F (D))$
27	22	adantr	$⊢ ((((F {Isom}_{R, S} (A, B) \land C \subseteq A) \land D \in A) \land y \in A) \land z \in C) \to F {Isom}_{R, S} (A, B)$
28		simplr	$⊢ ((((F {Isom}_{R, S} (A, B) \land C \subseteq A) \land D \in A) \land y \in A) \land z \in C) \to y \in A$
29	7	adantr	$⊢ (((F {Isom}_{R, S} (A, B) \land C \subseteq A) \land D \in A) \land y \in A) \to C \subseteq A$
30	29	sselda	$⊢ ((((F {Isom}_{R, S} (A, B) \land C \subseteq A) \land D \in A) \land y \in A) \land z \in C) \to z \in A$
31		isorel	$⊢ (F {Isom}_{R, S} (A, B) \land (y \in A \land z \in A)) \to (y R z \leftrightarrow F (y) S F (z))$
32	27 28 30 31	syl12anc	$⊢ ((((F {Isom}_{R, S} (A, B) \land C \subseteq A) \land D \in A) \land y \in A) \land z \in C) \to (y R z \leftrightarrow F (y) S F (z))$
33	32	rexbidva	$⊢ (((F {Isom}_{R, S} (A, B) \land C \subseteq A) \land D \in A) \land y \in A) \to (\exists z \in C y R z \leftrightarrow \exists z \in C F (y) S F (z))$
34	16	adantr	$⊢ (((F {Isom}_{R, S} (A, B) \land C \subseteq A) \land D \in A) \land y \in A) \to F Fn A$
35		breq2	$⊢ v = F (z) \to (F (y) S v \leftrightarrow F (y) S F (z))$
36	35	rexima	$⊢ (F Fn A \land C \subseteq A) \to (\exists v \in F [C] F (y) S v \leftrightarrow \exists z \in C F (y) S F (z))$
37	34 29 36	syl2anc	$⊢ (((F {Isom}_{R, S} (A, B) \land C \subseteq A) \land D \in A) \land y \in A) \to (\exists v \in F [C] F (y) S v \leftrightarrow \exists z \in C F (y) S F (z))$
38	33 37	bitr4d	$⊢ (((F {Isom}_{R, S} (A, B) \land C \subseteq A) \land D \in A) \land y \in A) \to (\exists z \in C y R z \leftrightarrow \exists v \in F [C] F (y) S v)$
39	26 38	imbi12d	$⊢ (((F {Isom}_{R, S} (A, B) \land C \subseteq A) \land D \in A) \land y \in A) \to ((y R D \to \exists z \in C y R z) \leftrightarrow (F (y) S F (D) \to \exists v \in F [C] F (y) S v))$
40	39	ralbidva	$⊢ ((F {Isom}_{R, S} (A, B) \land C \subseteq A) \land D \in A) \to (\forall y \in A (y R D \to \exists z \in C y R z) \leftrightarrow \forall y \in A (F (y) S F (D) \to \exists v \in F [C] F (y) S v))$
41		f1ofo	$⊢ F : A \underset{1-1 onto}{⟶} B \to F : A \underset{onto}{⟶} B$
42		breq1	$⊢ F (y) = w \to (F (y) S F (D) \leftrightarrow w S F (D))$
43		breq1	$⊢ F (y) = w \to (F (y) S v \leftrightarrow w S v)$
44	43	rexbidv	$⊢ F (y) = w \to (\exists v \in F [C] F (y) S v \leftrightarrow \exists v \in F [C] w S v)$
45	42 44	imbi12d	$⊢ F (y) = w \to ((F (y) S F (D) \to \exists v \in F [C] F (y) S v) \leftrightarrow (w S F (D) \to \exists v \in F [C] w S v))$
46	45	cbvfo	$⊢ F : A \underset{onto}{⟶} B \to (\forall y \in A (F (y) S F (D) \to \exists v \in F [C] F (y) S v) \leftrightarrow \forall w \in B (w S F (D) \to \exists v \in F [C] w S v))$
47	14 41 46	3syl	$⊢ ((F {Isom}_{R, S} (A, B) \land C \subseteq A) \land D \in A) \to (\forall y \in A (F (y) S F (D) \to \exists v \in F [C] F (y) S v) \leftrightarrow \forall w \in B (w S F (D) \to \exists v \in F [C] w S v))$
48	40 47	bitrd	$⊢ ((F {Isom}_{R, S} (A, B) \land C \subseteq A) \land D \in A) \to (\forall y \in A (y R D \to \exists z \in C y R z) \leftrightarrow \forall w \in B (w S F (D) \to \exists v \in F [C] w S v))$
49	21 48	anbi12d	$⊢ ((F {Isom}_{R, S} (A, B) \land C \subseteq A) \land D \in A) \to ((\forall y \in C \neg D R y \land \forall y \in A (y R D \to \exists z \in C y R z)) \leftrightarrow (\forall w \in F [C] \neg F (D) S w \land \forall w \in B (w S F (D) \to \exists v \in F [C] w S v)))$
50	3 49	sylan	$⊢ (φ \land D \in A) \to ((\forall y \in C \neg D R y \land \forall y \in A (y R D \to \exists z \in C y R z)) \leftrightarrow (\forall w \in F [C] \neg F (D) S w \land \forall w \in B (w S F (D) \to \exists v \in F [C] w S v)))$

Metamath Proof Explorer

Theorem supisolem

Proof