isoun

Description: Infer an isomorphism from a union of two isomorphisms. (Contributed by Thierry Arnoux, 30-Mar-2017)

	Ref	Expression
Hypotheses	isoun.1	$⊢ φ \to H {Isom}_{R, S} (A, B)$
	isoun.2	$⊢ φ \to G {Isom}_{R, S} (C, D)$
	isoun.3	$⊢ (φ \land x \in A \land y \in C) \to x R y$
	isoun.4	$⊢ (φ \land z \in B \land w \in D) \to z S w$
	isoun.5	$⊢ (φ \land x \in C \land y \in A) \to \neg x R y$
	isoun.6	$⊢ (φ \land z \in D \land w \in B) \to \neg z S w$
	isoun.7	$⊢ φ \to A \cap C = \emptyset$
	isoun.8	$⊢ φ \to B \cap D = \emptyset$
Assertion	isoun	$⊢ φ \to (H \cup G) {Isom}_{R, S} (A \cup C, B \cup D)$

Proof

Step	Hyp	Ref	Expression
1		isoun.1	$⊢ φ \to H {Isom}_{R, S} (A, B)$
2		isoun.2	$⊢ φ \to G {Isom}_{R, S} (C, D)$
3		isoun.3	$⊢ (φ \land x \in A \land y \in C) \to x R y$
4		isoun.4	$⊢ (φ \land z \in B \land w \in D) \to z S w$
5		isoun.5	$⊢ (φ \land x \in C \land y \in A) \to \neg x R y$
6		isoun.6	$⊢ (φ \land z \in D \land w \in B) \to \neg z S w$
7		isoun.7	$⊢ φ \to A \cap C = \emptyset$
8		isoun.8	$⊢ φ \to B \cap D = \emptyset$
9		isof1o	$⊢ H {Isom}_{R, S} (A, B) \to H : A \underset{1-1 onto}{⟶} B$
10	1 9	syl	$⊢ φ \to H : A \underset{1-1 onto}{⟶} B$
11		isof1o	$⊢ G {Isom}_{R, S} (C, D) \to G : C \underset{1-1 onto}{⟶} D$
12	2 11	syl	$⊢ φ \to G : C \underset{1-1 onto}{⟶} D$
13		f1oun	$⊢ ((H : A \underset{1-1 onto}{⟶} B \land G : C \underset{1-1 onto}{⟶} D) \land (A \cap C = \emptyset \land B \cap D = \emptyset)) \to (H \cup G) : A \cup C \underset{1-1 onto}{⟶} B \cup D$
14	10 12 7 8 13	syl22anc	$⊢ φ \to (H \cup G) : A \cup C \underset{1-1 onto}{⟶} B \cup D$
15		elun	$⊢ x \in (A \cup C) \leftrightarrow (x \in A \lor x \in C)$
16		elun	$⊢ y \in (A \cup C) \leftrightarrow (y \in A \lor y \in C)$
17		isorel	$⊢ (H {Isom}_{R, S} (A, B) \land (x \in A \land y \in A)) \to (x R y \leftrightarrow H (x) S H (y))$
18	1 17	sylan	$⊢ (φ \land (x \in A \land y \in A)) \to (x R y \leftrightarrow H (x) S H (y))$
19		f1ofn	$⊢ H : A \underset{1-1 onto}{⟶} B \to H Fn A$
20	10 19	syl	$⊢ φ \to H Fn A$
21	20	adantr	$⊢ (φ \land x \in A) \to H Fn A$
22		f1ofn	$⊢ G : C \underset{1-1 onto}{⟶} D \to G Fn C$
23	12 22	syl	$⊢ φ \to G Fn C$
24	23	adantr	$⊢ (φ \land x \in A) \to G Fn C$
25	7	anim1i	$⊢ (φ \land x \in A) \to (A \cap C = \emptyset \land x \in A)$
26		fvun1	$⊢ (H Fn A \land G Fn C \land (A \cap C = \emptyset \land x \in A)) \to (H \cup G) (x) = H (x)$
27	21 24 25 26	syl3anc	$⊢ (φ \land x \in A) \to (H \cup G) (x) = H (x)$
28	27	adantrr	$⊢ (φ \land (x \in A \land y \in A)) \to (H \cup G) (x) = H (x)$
29	20	adantr	$⊢ (φ \land y \in A) \to H Fn A$
30	23	adantr	$⊢ (φ \land y \in A) \to G Fn C$
31	7	anim1i	$⊢ (φ \land y \in A) \to (A \cap C = \emptyset \land y \in A)$
32		fvun1	$⊢ (H Fn A \land G Fn C \land (A \cap C = \emptyset \land y \in A)) \to (H \cup G) (y) = H (y)$
33	29 30 31 32	syl3anc	$⊢ (φ \land y \in A) \to (H \cup G) (y) = H (y)$
34	33	adantrl	$⊢ (φ \land (x \in A \land y \in A)) \to (H \cup G) (y) = H (y)$
35	28 34	breq12d	$⊢ (φ \land (x \in A \land y \in A)) \to ((H \cup G) (x) S (H \cup G) (y) \leftrightarrow H (x) S H (y))$
36	18 35	bitr4d	$⊢ (φ \land (x \in A \land y \in A)) \to (x R y \leftrightarrow (H \cup G) (x) S (H \cup G) (y))$
37	36	anassrs	$⊢ ((φ \land x \in A) \land y \in A) \to (x R y \leftrightarrow (H \cup G) (x) S (H \cup G) (y))$
38	3	3expb	$⊢ (φ \land (x \in A \land y \in C)) \to x R y$
39	4	3expia	$⊢ (φ \land z \in B) \to (w \in D \to z S w)$
40	39	ralrimiv	$⊢ (φ \land z \in B) \to \forall w \in D z S w$
41	40	ralrimiva	$⊢ φ \to \forall z \in B \forall w \in D z S w$
42	41	adantr	$⊢ (φ \land (x \in A \land y \in C)) \to \forall z \in B \forall w \in D z S w$
43		f1of	$⊢ H : A \underset{1-1 onto}{⟶} B \to H : A ⟶ B$
44	10 43	syl	$⊢ φ \to H : A ⟶ B$
45	44	ffvelrnda	$⊢ (φ \land x \in A) \to H (x) \in B$
46	45	adantrr	$⊢ (φ \land (x \in A \land y \in C)) \to H (x) \in B$
47		f1of	$⊢ G : C \underset{1-1 onto}{⟶} D \to G : C ⟶ D$
48	12 47	syl	$⊢ φ \to G : C ⟶ D$
49	48	ffvelrnda	$⊢ (φ \land y \in C) \to G (y) \in D$
50	49	adantrl	$⊢ (φ \land (x \in A \land y \in C)) \to G (y) \in D$
51		breq1	$⊢ z = H (x) \to (z S w \leftrightarrow H (x) S w)$
52		breq2	$⊢ w = G (y) \to (H (x) S w \leftrightarrow H (x) S G (y))$
53	51 52	rspc2v	$⊢ (H (x) \in B \land G (y) \in D) \to (\forall z \in B \forall w \in D z S w \to H (x) S G (y))$
54	46 50 53	syl2anc	$⊢ (φ \land (x \in A \land y \in C)) \to (\forall z \in B \forall w \in D z S w \to H (x) S G (y))$
55	42 54	mpd	$⊢ (φ \land (x \in A \land y \in C)) \to H (x) S G (y)$
56	27	adantrr	$⊢ (φ \land (x \in A \land y \in C)) \to (H \cup G) (x) = H (x)$
57	20	adantr	$⊢ (φ \land y \in C) \to H Fn A$
58	23	adantr	$⊢ (φ \land y \in C) \to G Fn C$
59	7	anim1i	$⊢ (φ \land y \in C) \to (A \cap C = \emptyset \land y \in C)$
60		fvun2	$⊢ (H Fn A \land G Fn C \land (A \cap C = \emptyset \land y \in C)) \to (H \cup G) (y) = G (y)$
61	57 58 59 60	syl3anc	$⊢ (φ \land y \in C) \to (H \cup G) (y) = G (y)$
62	61	adantrl	$⊢ (φ \land (x \in A \land y \in C)) \to (H \cup G) (y) = G (y)$
63	55 56 62	3brtr4d	$⊢ (φ \land (x \in A \land y \in C)) \to (H \cup G) (x) S (H \cup G) (y)$
64	38 63	2thd	$⊢ (φ \land (x \in A \land y \in C)) \to (x R y \leftrightarrow (H \cup G) (x) S (H \cup G) (y))$
65	64	anassrs	$⊢ ((φ \land x \in A) \land y \in C) \to (x R y \leftrightarrow (H \cup G) (x) S (H \cup G) (y))$
66	37 65	jaodan	$⊢ ((φ \land x \in A) \land (y \in A \lor y \in C)) \to (x R y \leftrightarrow (H \cup G) (x) S (H \cup G) (y))$
67	16 66	sylan2b	$⊢ ((φ \land x \in A) \land y \in (A \cup C)) \to (x R y \leftrightarrow (H \cup G) (x) S (H \cup G) (y))$
68	67	ex	$⊢ (φ \land x \in A) \to (y \in (A \cup C) \to (x R y \leftrightarrow (H \cup G) (x) S (H \cup G) (y)))$
69	5	3expb	$⊢ (φ \land (x \in C \land y \in A)) \to \neg x R y$
70	6	3expia	$⊢ (φ \land z \in D) \to (w \in B \to \neg z S w)$
71	70	ralrimiv	$⊢ (φ \land z \in D) \to \forall w \in B \neg z S w$
72	71	ralrimiva	$⊢ φ \to \forall z \in D \forall w \in B \neg z S w$
73	72	adantr	$⊢ (φ \land (x \in C \land y \in A)) \to \forall z \in D \forall w \in B \neg z S w$
74	48	ffvelrnda	$⊢ (φ \land x \in C) \to G (x) \in D$
75	74	adantrr	$⊢ (φ \land (x \in C \land y \in A)) \to G (x) \in D$
76	44	ffvelrnda	$⊢ (φ \land y \in A) \to H (y) \in B$
77	76	adantrl	$⊢ (φ \land (x \in C \land y \in A)) \to H (y) \in B$
78		breq1	$⊢ z = G (x) \to (z S w \leftrightarrow G (x) S w)$
79	78	notbid	$⊢ z = G (x) \to (\neg z S w \leftrightarrow \neg G (x) S w)$
80		breq2	$⊢ w = H (y) \to (G (x) S w \leftrightarrow G (x) S H (y))$
81	80	notbid	$⊢ w = H (y) \to (\neg G (x) S w \leftrightarrow \neg G (x) S H (y))$
82	79 81	rspc2v	$⊢ (G (x) \in D \land H (y) \in B) \to (\forall z \in D \forall w \in B \neg z S w \to \neg G (x) S H (y))$
83	75 77 82	syl2anc	$⊢ (φ \land (x \in C \land y \in A)) \to (\forall z \in D \forall w \in B \neg z S w \to \neg G (x) S H (y))$
84	73 83	mpd	$⊢ (φ \land (x \in C \land y \in A)) \to \neg G (x) S H (y)$
85	20	adantr	$⊢ (φ \land x \in C) \to H Fn A$
86	23	adantr	$⊢ (φ \land x \in C) \to G Fn C$
87	7	anim1i	$⊢ (φ \land x \in C) \to (A \cap C = \emptyset \land x \in C)$
88		fvun2	$⊢ (H Fn A \land G Fn C \land (A \cap C = \emptyset \land x \in C)) \to (H \cup G) (x) = G (x)$
89	85 86 87 88	syl3anc	$⊢ (φ \land x \in C) \to (H \cup G) (x) = G (x)$
90	89	adantrr	$⊢ (φ \land (x \in C \land y \in A)) \to (H \cup G) (x) = G (x)$
91	33	adantrl	$⊢ (φ \land (x \in C \land y \in A)) \to (H \cup G) (y) = H (y)$
92	90 91	breq12d	$⊢ (φ \land (x \in C \land y \in A)) \to ((H \cup G) (x) S (H \cup G) (y) \leftrightarrow G (x) S H (y))$
93	84 92	mtbird	$⊢ (φ \land (x \in C \land y \in A)) \to \neg (H \cup G) (x) S (H \cup G) (y)$
94	69 93	2falsed	$⊢ (φ \land (x \in C \land y \in A)) \to (x R y \leftrightarrow (H \cup G) (x) S (H \cup G) (y))$
95	94	anassrs	$⊢ ((φ \land x \in C) \land y \in A) \to (x R y \leftrightarrow (H \cup G) (x) S (H \cup G) (y))$
96		isorel	$⊢ (G {Isom}_{R, S} (C, D) \land (x \in C \land y \in C)) \to (x R y \leftrightarrow G (x) S G (y))$
97	2 96	sylan	$⊢ (φ \land (x \in C \land y \in C)) \to (x R y \leftrightarrow G (x) S G (y))$
98	89	adantrr	$⊢ (φ \land (x \in C \land y \in C)) \to (H \cup G) (x) = G (x)$
99	61	adantrl	$⊢ (φ \land (x \in C \land y \in C)) \to (H \cup G) (y) = G (y)$
100	98 99	breq12d	$⊢ (φ \land (x \in C \land y \in C)) \to ((H \cup G) (x) S (H \cup G) (y) \leftrightarrow G (x) S G (y))$
101	97 100	bitr4d	$⊢ (φ \land (x \in C \land y \in C)) \to (x R y \leftrightarrow (H \cup G) (x) S (H \cup G) (y))$
102	101	anassrs	$⊢ ((φ \land x \in C) \land y \in C) \to (x R y \leftrightarrow (H \cup G) (x) S (H \cup G) (y))$
103	95 102	jaodan	$⊢ ((φ \land x \in C) \land (y \in A \lor y \in C)) \to (x R y \leftrightarrow (H \cup G) (x) S (H \cup G) (y))$
104	16 103	sylan2b	$⊢ ((φ \land x \in C) \land y \in (A \cup C)) \to (x R y \leftrightarrow (H \cup G) (x) S (H \cup G) (y))$
105	104	ex	$⊢ (φ \land x \in C) \to (y \in (A \cup C) \to (x R y \leftrightarrow (H \cup G) (x) S (H \cup G) (y)))$
106	68 105	jaodan	$⊢ (φ \land (x \in A \lor x \in C)) \to (y \in (A \cup C) \to (x R y \leftrightarrow (H \cup G) (x) S (H \cup G) (y)))$
107	15 106	sylan2b	$⊢ (φ \land x \in (A \cup C)) \to (y \in (A \cup C) \to (x R y \leftrightarrow (H \cup G) (x) S (H \cup G) (y)))$
108	107	ralrimiv	$⊢ (φ \land x \in (A \cup C)) \to \forall y \in (A \cup C) (x R y \leftrightarrow (H \cup G) (x) S (H \cup G) (y))$
109	108	ralrimiva	$⊢ φ \to \forall x \in (A \cup C) \forall y \in (A \cup C) (x R y \leftrightarrow (H \cup G) (x) S (H \cup G) (y))$
110		df-isom	$⊢ (H \cup G) {Isom}_{R, S} (A \cup C, B \cup D) \leftrightarrow ((H \cup G) : A \cup C \underset{1-1 onto}{⟶} B \cup D \land \forall x \in (A \cup C) \forall y \in (A \cup C) (x R y \leftrightarrow (H \cup G) (x) S (H \cup G) (y)))$
111	14 109 110	sylanbrc	$⊢ φ \to (H \cup G) {Isom}_{R, S} (A \cup C, B \cup D)$

Metamath Proof Explorer

Theorem isoun

Proof