erdsze2lem2

	Ref	Expression
Hypotheses	erdsze2.r	$⊢ φ \to R \in ℕ$
	erdsze2.s	$⊢ φ \to S \in ℕ$
	erdsze2.f	$⊢ φ \to F : A \underset{1-1}{⟶} ℝ$
	erdsze2.a	$⊢ φ \to A \subseteq ℝ$
	erdsze2lem.n	$⊢ N = (R - 1) (S - 1)$
	erdsze2lem.l	$⊢ φ \to N < \|A\|$
	erdsze2lem.g	$⊢ φ \to G : (1 \dots N + 1) \underset{1-1}{⟶} A$
	erdsze2lem.i	$⊢ φ \to G {Isom}_{<, <} ((1 \dots N + 1), ran G)$
Assertion	erdsze2lem2	$⊢ φ \to \exists s \in 𝒫 A ((R \leq \|s\| \land ({F ↾}_{s}) {Isom}_{<, <} (s, F [s])) \lor (S \leq \|s\| \land ({F ↾}_{s}) {Isom}_{<, <^{-1}} (s, F [s])))$

Proof

Step	Hyp	Ref	Expression
1		erdsze2.r	$⊢ φ \to R \in ℕ$
2		erdsze2.s	$⊢ φ \to S \in ℕ$
3		erdsze2.f	$⊢ φ \to F : A \underset{1-1}{⟶} ℝ$
4		erdsze2.a	$⊢ φ \to A \subseteq ℝ$
5		erdsze2lem.n	$⊢ N = (R - 1) (S - 1)$
6		erdsze2lem.l	$⊢ φ \to N < \|A\|$
7		erdsze2lem.g	$⊢ φ \to G : (1 \dots N + 1) \underset{1-1}{⟶} A$
8		erdsze2lem.i	$⊢ φ \to G {Isom}_{<, <} ((1 \dots N + 1), ran G)$
9		nnm1nn0	$⊢ R \in ℕ \to R - 1 \in ℕ_{0}$
10	1 9	syl	$⊢ φ \to R - 1 \in ℕ_{0}$
11		nnm1nn0	$⊢ S \in ℕ \to S - 1 \in ℕ_{0}$
12	2 11	syl	$⊢ φ \to S - 1 \in ℕ_{0}$
13	10 12	nn0mulcld	$⊢ φ \to (R - 1) (S - 1) \in ℕ_{0}$
14	5 13	eqeltrid	$⊢ φ \to N \in ℕ_{0}$
15		nn0p1nn	$⊢ N \in ℕ_{0} \to N + 1 \in ℕ$
16	14 15	syl	$⊢ φ \to N + 1 \in ℕ$
17		f1co	$⊢ (F : A \underset{1-1}{⟶} ℝ \land G : (1 \dots N + 1) \underset{1-1}{⟶} A) \to (F \circ G) : (1 \dots N + 1) \underset{1-1}{⟶} ℝ$
18	3 7 17	syl2anc	$⊢ φ \to (F \circ G) : (1 \dots N + 1) \underset{1-1}{⟶} ℝ$
19	14	nn0red	$⊢ φ \to N \in ℝ$
20	19	ltp1d	$⊢ φ \to N < N + 1$
21	5 20	eqbrtrrid	$⊢ φ \to (R - 1) (S - 1) < N + 1$
22	16 18 1 2 21	erdsze	$⊢ φ \to \exists t \in 𝒫 (1 \dots N + 1) ((R \leq \|t\| \land ({(F \circ G) ↾}_{t}) {Isom}_{<, <} (t, (F \circ G) [t])) \lor (S \leq \|t\| \land ({(F \circ G) ↾}_{t}) {Isom}_{<, <^{-1}} (t, (F \circ G) [t])))$
23		velpw	$⊢ t \in 𝒫 (1 \dots N + 1) \leftrightarrow t \subseteq (1 \dots N + 1)$
24		imassrn	$⊢ G [t] \subseteq ran G$
25		f1f	$⊢ G : (1 \dots N + 1) \underset{1-1}{⟶} A \to G : (1 \dots N + 1) ⟶ A$
26	7 25	syl	$⊢ φ \to G : (1 \dots N + 1) ⟶ A$
27	26	frnd	$⊢ φ \to ran G \subseteq A$
28	24 27	sstrid	$⊢ φ \to G [t] \subseteq A$
29		reex	$⊢ ℝ \in V$
30		ssexg	$⊢ (A \subseteq ℝ \land ℝ \in V) \to A \in V$
31	4 29 30	sylancl	$⊢ φ \to A \in V$
32		elpw2g	$⊢ A \in V \to (G [t] \in 𝒫 A \leftrightarrow G [t] \subseteq A)$
33	31 32	syl	$⊢ φ \to (G [t] \in 𝒫 A \leftrightarrow G [t] \subseteq A)$
34	28 33	mpbird	$⊢ φ \to G [t] \in 𝒫 A$
35	34	adantr	$⊢ (φ \land t \subseteq (1 \dots N + 1)) \to G [t] \in 𝒫 A$
36		vex	$⊢ t \in V$
37	36	f1imaen	$⊢ (G : (1 \dots N + 1) \underset{1-1}{⟶} A \land t \subseteq (1 \dots N + 1)) \to G [t] \approx t$
38	7 37	sylan	$⊢ (φ \land t \subseteq (1 \dots N + 1)) \to G [t] \approx t$
39		fzfid	$⊢ (φ \land t \subseteq (1 \dots N + 1)) \to (1 \dots N + 1) \in Fin$
40		simpr	$⊢ (φ \land t \subseteq (1 \dots N + 1)) \to t \subseteq (1 \dots N + 1)$
41		ssfi	$⊢ ((1 \dots N + 1) \in Fin \land t \subseteq (1 \dots N + 1)) \to t \in Fin$
42	39 40 41	syl2anc	$⊢ (φ \land t \subseteq (1 \dots N + 1)) \to t \in Fin$
43		enfii	$⊢ (t \in Fin \land G [t] \approx t) \to G [t] \in Fin$
44	42 38 43	syl2anc	$⊢ (φ \land t \subseteq (1 \dots N + 1)) \to G [t] \in Fin$
45		hashen	$⊢ (G [t] \in Fin \land t \in Fin) \to (\|G [t]\| = \|t\| \leftrightarrow G [t] \approx t)$
46	44 42 45	syl2anc	$⊢ (φ \land t \subseteq (1 \dots N + 1)) \to (\|G [t]\| = \|t\| \leftrightarrow G [t] \approx t)$
47	38 46	mpbird	$⊢ (φ \land t \subseteq (1 \dots N + 1)) \to \|G [t]\| = \|t\|$
48	47	breq2d	$⊢ (φ \land t \subseteq (1 \dots N + 1)) \to (R \leq \|G [t]\| \leftrightarrow R \leq \|t\|)$
49	48	biimprd	$⊢ (φ \land t \subseteq (1 \dots N + 1)) \to (R \leq \|t\| \to R \leq \|G [t]\|)$
50	8	ad2antrr	$⊢ ((φ \land t \subseteq (1 \dots N + 1)) \land (x \in t \land y \in t)) \to G {Isom}_{<, <} ((1 \dots N + 1), ran G)$
51	40	adantr	$⊢ ((φ \land t \subseteq (1 \dots N + 1)) \land (x \in t \land y \in t)) \to t \subseteq (1 \dots N + 1)$
52		simprl	$⊢ ((φ \land t \subseteq (1 \dots N + 1)) \land (x \in t \land y \in t)) \to x \in t$
53	51 52	sseldd	$⊢ ((φ \land t \subseteq (1 \dots N + 1)) \land (x \in t \land y \in t)) \to x \in (1 \dots N + 1)$
54		simprr	$⊢ ((φ \land t \subseteq (1 \dots N + 1)) \land (x \in t \land y \in t)) \to y \in t$
55	51 54	sseldd	$⊢ ((φ \land t \subseteq (1 \dots N + 1)) \land (x \in t \land y \in t)) \to y \in (1 \dots N + 1)$
56		isorel	$⊢ (G {Isom}_{<, <} ((1 \dots N + 1), ran G) \land (x \in (1 \dots N + 1) \land y \in (1 \dots N + 1))) \to (x < y \leftrightarrow G (x) < G (y))$
57	50 53 55 56	syl12anc	$⊢ ((φ \land t \subseteq (1 \dots N + 1)) \land (x \in t \land y \in t)) \to (x < y \leftrightarrow G (x) < G (y))$
58	57	biimpd	$⊢ ((φ \land t \subseteq (1 \dots N + 1)) \land (x \in t \land y \in t)) \to (x < y \to G (x) < G (y))$
59	58	ralrimivva	$⊢ (φ \land t \subseteq (1 \dots N + 1)) \to \forall x \in t \forall y \in t (x < y \to G (x) < G (y))$
60		elfznn	$⊢ t \in (1 \dots N + 1) \to t \in ℕ$
61	60	nnred	$⊢ t \in (1 \dots N + 1) \to t \in ℝ$
62	61	ssriv	$⊢ (1 \dots N + 1) \subseteq ℝ$
63	62	a1i	$⊢ (φ \land t \subseteq (1 \dots N + 1)) \to (1 \dots N + 1) \subseteq ℝ$
64		ltso	$⊢ < Or ℝ$
65		soss	$⊢ (1 \dots N + 1) \subseteq ℝ \to (< Or ℝ \to < Or (1 \dots N + 1))$
66	63 64 65	mpisyl	$⊢ (φ \land t \subseteq (1 \dots N + 1)) \to < Or (1 \dots N + 1)$
67	4	adantr	$⊢ (φ \land t \subseteq (1 \dots N + 1)) \to A \subseteq ℝ$
68		soss	$⊢ A \subseteq ℝ \to (< Or ℝ \to < Or A)$
69	67 64 68	mpisyl	$⊢ (φ \land t \subseteq (1 \dots N + 1)) \to < Or A$
70	26	adantr	$⊢ (φ \land t \subseteq (1 \dots N + 1)) \to G : (1 \dots N + 1) ⟶ A$
71		soisores	$⊢ ((< Or (1 \dots N + 1) \land < Or A) \land (G : (1 \dots N + 1) ⟶ A \land t \subseteq (1 \dots N + 1))) \to (({G ↾}_{t}) {Isom}_{<, <} (t, G [t]) \leftrightarrow \forall x \in t \forall y \in t (x < y \to G (x) < G (y)))$
72	66 69 70 40 71	syl22anc	$⊢ (φ \land t \subseteq (1 \dots N + 1)) \to (({G ↾}_{t}) {Isom}_{<, <} (t, G [t]) \leftrightarrow \forall x \in t \forall y \in t (x < y \to G (x) < G (y)))$
73	59 72	mpbird	$⊢ (φ \land t \subseteq (1 \dots N + 1)) \to ({G ↾}_{t}) {Isom}_{<, <} (t, G [t])$
74		isocnv	$⊢ ({G ↾}_{t}) {Isom}_{<, <} (t, G [t]) \to {({G ↾}_{t})}^{-1} {Isom}_{<, <} (G [t], t)$
75	73 74	syl	$⊢ (φ \land t \subseteq (1 \dots N + 1)) \to {({G ↾}_{t})}^{-1} {Isom}_{<, <} (G [t], t)$
76		isotr	$⊢ ({({G ↾}_{t})}^{-1} {Isom}_{<, <} (G [t], t) \land ({(F \circ G) ↾}_{t}) {Isom}_{<, <} (t, (F \circ G) [t])) \to (({(F \circ G) ↾}_{t}) \circ {({G ↾}_{t})}^{-1}) {Isom}_{<, <} (G [t], (F \circ G) [t])$
77	76	ex	$⊢ {({G ↾}_{t})}^{-1} {Isom}_{<, <} (G [t], t) \to (({(F \circ G) ↾}_{t}) {Isom}_{<, <} (t, (F \circ G) [t]) \to (({(F \circ G) ↾}_{t}) \circ {({G ↾}_{t})}^{-1}) {Isom}_{<, <} (G [t], (F \circ G) [t]))$
78	75 77	syl	$⊢ (φ \land t \subseteq (1 \dots N + 1)) \to (({(F \circ G) ↾}_{t}) {Isom}_{<, <} (t, (F \circ G) [t]) \to (({(F \circ G) ↾}_{t}) \circ {({G ↾}_{t})}^{-1}) {Isom}_{<, <} (G [t], (F \circ G) [t]))$
79		resco	$⊢ {(F \circ G) ↾}_{t} = F \circ ({G ↾}_{t})$
80	79	coeq1i	$⊢ ({(F \circ G) ↾}_{t}) \circ {({G ↾}_{t})}^{-1} = (F \circ ({G ↾}_{t})) \circ {({G ↾}_{t})}^{-1}$
81		coass	$⊢ (F \circ ({G ↾}_{t})) \circ {({G ↾}_{t})}^{-1} = F \circ (({G ↾}_{t}) \circ {({G ↾}_{t})}^{-1})$
82	80 81	eqtri	$⊢ ({(F \circ G) ↾}_{t}) \circ {({G ↾}_{t})}^{-1} = F \circ (({G ↾}_{t}) \circ {({G ↾}_{t})}^{-1})$
83		f1ores	$⊢ (G : (1 \dots N + 1) \underset{1-1}{⟶} A \land t \subseteq (1 \dots N + 1)) \to ({G ↾}_{t}) : t \underset{1-1 onto}{⟶} G [t]$
84	7 83	sylan	$⊢ (φ \land t \subseteq (1 \dots N + 1)) \to ({G ↾}_{t}) : t \underset{1-1 onto}{⟶} G [t]$
85		f1ococnv2	$⊢ ({G ↾}_{t}) : t \underset{1-1 onto}{⟶} G [t] \to ({G ↾}_{t}) \circ {({G ↾}_{t})}^{-1} = {I ↾}_{G [t]}$
86	84 85	syl	$⊢ (φ \land t \subseteq (1 \dots N + 1)) \to ({G ↾}_{t}) \circ {({G ↾}_{t})}^{-1} = {I ↾}_{G [t]}$
87	86	coeq2d	$⊢ (φ \land t \subseteq (1 \dots N + 1)) \to F \circ (({G ↾}_{t}) \circ {({G ↾}_{t})}^{-1}) = F \circ ({I ↾}_{G [t]})$
88		coires1	$⊢ F \circ ({I ↾}_{G [t]}) = {F ↾}_{G [t]}$
89	87 88	eqtrdi	$⊢ (φ \land t \subseteq (1 \dots N + 1)) \to F \circ (({G ↾}_{t}) \circ {({G ↾}_{t})}^{-1}) = {F ↾}_{G [t]}$
90	82 89	syl5eq	$⊢ (φ \land t \subseteq (1 \dots N + 1)) \to ({(F \circ G) ↾}_{t}) \circ {({G ↾}_{t})}^{-1} = {F ↾}_{G [t]}$
91		isoeq1	$⊢ ({(F \circ G) ↾}_{t}) \circ {({G ↾}_{t})}^{-1} = {F ↾}_{G [t]} \to ((({(F \circ G) ↾}_{t}) \circ {({G ↾}_{t})}^{-1}) {Isom}_{<, <} (G [t], (F \circ G) [t]) \leftrightarrow ({F ↾}_{G [t]}) {Isom}_{<, <} (G [t], (F \circ G) [t]))$
92	90 91	syl	$⊢ (φ \land t \subseteq (1 \dots N + 1)) \to ((({(F \circ G) ↾}_{t}) \circ {({G ↾}_{t})}^{-1}) {Isom}_{<, <} (G [t], (F \circ G) [t]) \leftrightarrow ({F ↾}_{G [t]}) {Isom}_{<, <} (G [t], (F \circ G) [t]))$
93		imaco	$⊢ (F \circ G) [t] = F [G [t]]$
94		isoeq5	$⊢ (F \circ G) [t] = F [G [t]] \to (({F ↾}_{G [t]}) {Isom}_{<, <} (G [t], (F \circ G) [t]) \leftrightarrow ({F ↾}_{G [t]}) {Isom}_{<, <} (G [t], F [G [t]]))$
95	93 94	ax-mp	$⊢ ({F ↾}_{G [t]}) {Isom}_{<, <} (G [t], (F \circ G) [t]) \leftrightarrow ({F ↾}_{G [t]}) {Isom}_{<, <} (G [t], F [G [t]])$
96	92 95	bitrdi	$⊢ (φ \land t \subseteq (1 \dots N + 1)) \to ((({(F \circ G) ↾}_{t}) \circ {({G ↾}_{t})}^{-1}) {Isom}_{<, <} (G [t], (F \circ G) [t]) \leftrightarrow ({F ↾}_{G [t]}) {Isom}_{<, <} (G [t], F [G [t]]))$
97	78 96	sylibd	$⊢ (φ \land t \subseteq (1 \dots N + 1)) \to (({(F \circ G) ↾}_{t}) {Isom}_{<, <} (t, (F \circ G) [t]) \to ({F ↾}_{G [t]}) {Isom}_{<, <} (G [t], F [G [t]]))$
98	49 97	anim12d	$⊢ (φ \land t \subseteq (1 \dots N + 1)) \to ((R \leq \|t\| \land ({(F \circ G) ↾}_{t}) {Isom}_{<, <} (t, (F \circ G) [t])) \to (R \leq \|G [t]\| \land ({F ↾}_{G [t]}) {Isom}_{<, <} (G [t], F [G [t]])))$
99	47	breq2d	$⊢ (φ \land t \subseteq (1 \dots N + 1)) \to (S \leq \|G [t]\| \leftrightarrow S \leq \|t\|)$
100	99	biimprd	$⊢ (φ \land t \subseteq (1 \dots N + 1)) \to (S \leq \|t\| \to S \leq \|G [t]\|)$
101		isotr	$⊢ ({({G ↾}_{t})}^{-1} {Isom}_{<, <} (G [t], t) \land ({(F \circ G) ↾}_{t}) {Isom}_{<, <^{-1}} (t, (F \circ G) [t])) \to (({(F \circ G) ↾}_{t}) \circ {({G ↾}_{t})}^{-1}) {Isom}_{<, <^{-1}} (G [t], (F \circ G) [t])$
102	101	ex	$⊢ {({G ↾}_{t})}^{-1} {Isom}_{<, <} (G [t], t) \to (({(F \circ G) ↾}_{t}) {Isom}_{<, <^{-1}} (t, (F \circ G) [t]) \to (({(F \circ G) ↾}_{t}) \circ {({G ↾}_{t})}^{-1}) {Isom}_{<, <^{-1}} (G [t], (F \circ G) [t]))$
103	75 102	syl	$⊢ (φ \land t \subseteq (1 \dots N + 1)) \to (({(F \circ G) ↾}_{t}) {Isom}_{<, <^{-1}} (t, (F \circ G) [t]) \to (({(F \circ G) ↾}_{t}) \circ {({G ↾}_{t})}^{-1}) {Isom}_{<, <^{-1}} (G [t], (F \circ G) [t]))$
104		isoeq1	$⊢ ({(F \circ G) ↾}_{t}) \circ {({G ↾}_{t})}^{-1} = {F ↾}_{G [t]} \to ((({(F \circ G) ↾}_{t}) \circ {({G ↾}_{t})}^{-1}) {Isom}_{<, <^{-1}} (G [t], (F \circ G) [t]) \leftrightarrow ({F ↾}_{G [t]}) {Isom}_{<, <^{-1}} (G [t], (F \circ G) [t]))$
105	90 104	syl	$⊢ (φ \land t \subseteq (1 \dots N + 1)) \to ((({(F \circ G) ↾}_{t}) \circ {({G ↾}_{t})}^{-1}) {Isom}_{<, <^{-1}} (G [t], (F \circ G) [t]) \leftrightarrow ({F ↾}_{G [t]}) {Isom}_{<, <^{-1}} (G [t], (F \circ G) [t]))$
106		isoeq5	$⊢ (F \circ G) [t] = F [G [t]] \to (({F ↾}_{G [t]}) {Isom}_{<, <^{-1}} (G [t], (F \circ G) [t]) \leftrightarrow ({F ↾}_{G [t]}) {Isom}_{<, <^{-1}} (G [t], F [G [t]]))$
107	93 106	ax-mp	$⊢ ({F ↾}_{G [t]}) {Isom}_{<, <^{-1}} (G [t], (F \circ G) [t]) \leftrightarrow ({F ↾}_{G [t]}) {Isom}_{<, <^{-1}} (G [t], F [G [t]])$
108	105 107	bitrdi	$⊢ (φ \land t \subseteq (1 \dots N + 1)) \to ((({(F \circ G) ↾}_{t}) \circ {({G ↾}_{t})}^{-1}) {Isom}_{<, <^{-1}} (G [t], (F \circ G) [t]) \leftrightarrow ({F ↾}_{G [t]}) {Isom}_{<, <^{-1}} (G [t], F [G [t]]))$
109	103 108	sylibd	$⊢ (φ \land t \subseteq (1 \dots N + 1)) \to (({(F \circ G) ↾}_{t}) {Isom}_{<, <^{-1}} (t, (F \circ G) [t]) \to ({F ↾}_{G [t]}) {Isom}_{<, <^{-1}} (G [t], F [G [t]]))$
110	100 109	anim12d	$⊢ (φ \land t \subseteq (1 \dots N + 1)) \to ((S \leq \|t\| \land ({(F \circ G) ↾}_{t}) {Isom}_{<, <^{-1}} (t, (F \circ G) [t])) \to (S \leq \|G [t]\| \land ({F ↾}_{G [t]}) {Isom}_{<, <^{-1}} (G [t], F [G [t]])))$
111	98 110	orim12d	$⊢ (φ \land t \subseteq (1 \dots N + 1)) \to (((R \leq \|t\| \land ({(F \circ G) ↾}_{t}) {Isom}_{<, <} (t, (F \circ G) [t])) \lor (S \leq \|t\| \land ({(F \circ G) ↾}_{t}) {Isom}_{<, <^{-1}} (t, (F \circ G) [t]))) \to ((R \leq \|G [t]\| \land ({F ↾}_{G [t]}) {Isom}_{<, <} (G [t], F [G [t]])) \lor (S \leq \|G [t]\| \land ({F ↾}_{G [t]}) {Isom}_{<, <^{-1}} (G [t], F [G [t]]))))$
112		fveq2	$⊢ s = G [t] \to \|s\| = \|G [t]\|$
113	112	breq2d	$⊢ s = G [t] \to (R \leq \|s\| \leftrightarrow R \leq \|G [t]\|)$
114		reseq2	$⊢ s = G [t] \to {F ↾}_{s} = {F ↾}_{G [t]}$
115		isoeq1	$⊢ {F ↾}_{s} = {F ↾}_{G [t]} \to (({F ↾}_{s}) {Isom}_{<, <} (s, F [s]) \leftrightarrow ({F ↾}_{G [t]}) {Isom}_{<, <} (s, F [s]))$
116	114 115	syl	$⊢ s = G [t] \to (({F ↾}_{s}) {Isom}_{<, <} (s, F [s]) \leftrightarrow ({F ↾}_{G [t]}) {Isom}_{<, <} (s, F [s]))$
117		isoeq4	$⊢ s = G [t] \to (({F ↾}_{G [t]}) {Isom}_{<, <} (s, F [s]) \leftrightarrow ({F ↾}_{G [t]}) {Isom}_{<, <} (G [t], F [s]))$
118		imaeq2	$⊢ s = G [t] \to F [s] = F [G [t]]$
119		isoeq5	$⊢ F [s] = F [G [t]] \to (({F ↾}_{G [t]}) {Isom}_{<, <} (G [t], F [s]) \leftrightarrow ({F ↾}_{G [t]}) {Isom}_{<, <} (G [t], F [G [t]]))$
120	118 119	syl	$⊢ s = G [t] \to (({F ↾}_{G [t]}) {Isom}_{<, <} (G [t], F [s]) \leftrightarrow ({F ↾}_{G [t]}) {Isom}_{<, <} (G [t], F [G [t]]))$
121	116 117 120	3bitrd	$⊢ s = G [t] \to (({F ↾}_{s}) {Isom}_{<, <} (s, F [s]) \leftrightarrow ({F ↾}_{G [t]}) {Isom}_{<, <} (G [t], F [G [t]]))$
122	113 121	anbi12d	$⊢ s = G [t] \to ((R \leq \|s\| \land ({F ↾}_{s}) {Isom}_{<, <} (s, F [s])) \leftrightarrow (R \leq \|G [t]\| \land ({F ↾}_{G [t]}) {Isom}_{<, <} (G [t], F [G [t]])))$
123	112	breq2d	$⊢ s = G [t] \to (S \leq \|s\| \leftrightarrow S \leq \|G [t]\|)$
124		isoeq1	$⊢ {F ↾}_{s} = {F ↾}_{G [t]} \to (({F ↾}_{s}) {Isom}_{<, <^{-1}} (s, F [s]) \leftrightarrow ({F ↾}_{G [t]}) {Isom}_{<, <^{-1}} (s, F [s]))$
125	114 124	syl	$⊢ s = G [t] \to (({F ↾}_{s}) {Isom}_{<, <^{-1}} (s, F [s]) \leftrightarrow ({F ↾}_{G [t]}) {Isom}_{<, <^{-1}} (s, F [s]))$
126		isoeq4	$⊢ s = G [t] \to (({F ↾}_{G [t]}) {Isom}_{<, <^{-1}} (s, F [s]) \leftrightarrow ({F ↾}_{G [t]}) {Isom}_{<, <^{-1}} (G [t], F [s]))$
127		isoeq5	$⊢ F [s] = F [G [t]] \to (({F ↾}_{G [t]}) {Isom}_{<, <^{-1}} (G [t], F [s]) \leftrightarrow ({F ↾}_{G [t]}) {Isom}_{<, <^{-1}} (G [t], F [G [t]]))$
128	118 127	syl	$⊢ s = G [t] \to (({F ↾}_{G [t]}) {Isom}_{<, <^{-1}} (G [t], F [s]) \leftrightarrow ({F ↾}_{G [t]}) {Isom}_{<, <^{-1}} (G [t], F [G [t]]))$
129	125 126 128	3bitrd	$⊢ s = G [t] \to (({F ↾}_{s}) {Isom}_{<, <^{-1}} (s, F [s]) \leftrightarrow ({F ↾}_{G [t]}) {Isom}_{<, <^{-1}} (G [t], F [G [t]]))$
130	123 129	anbi12d	$⊢ s = G [t] \to ((S \leq \|s\| \land ({F ↾}_{s}) {Isom}_{<, <^{-1}} (s, F [s])) \leftrightarrow (S \leq \|G [t]\| \land ({F ↾}_{G [t]}) {Isom}_{<, <^{-1}} (G [t], F [G [t]])))$
131	122 130	orbi12d	$⊢ s = G [t] \to (((R \leq \|s\| \land ({F ↾}_{s}) {Isom}_{<, <} (s, F [s])) \lor (S \leq \|s\| \land ({F ↾}_{s}) {Isom}_{<, <^{-1}} (s, F [s]))) \leftrightarrow ((R \leq \|G [t]\| \land ({F ↾}_{G [t]}) {Isom}_{<, <} (G [t], F [G [t]])) \lor (S \leq \|G [t]\| \land ({F ↾}_{G [t]}) {Isom}_{<, <^{-1}} (G [t], F [G [t]]))))$
132	131	rspcev	$⊢ (G [t] \in 𝒫 A \land ((R \leq \|G [t]\| \land ({F ↾}_{G [t]}) {Isom}_{<, <} (G [t], F [G [t]])) \lor (S \leq \|G [t]\| \land ({F ↾}_{G [t]}) {Isom}_{<, <^{-1}} (G [t], F [G [t]])))) \to \exists s \in 𝒫 A ((R \leq \|s\| \land ({F ↾}_{s}) {Isom}_{<, <} (s, F [s])) \lor (S \leq \|s\| \land ({F ↾}_{s}) {Isom}_{<, <^{-1}} (s, F [s])))$
133	35 111 132	syl6an	$⊢ (φ \land t \subseteq (1 \dots N + 1)) \to (((R \leq \|t\| \land ({(F \circ G) ↾}_{t}) {Isom}_{<, <} (t, (F \circ G) [t])) \lor (S \leq \|t\| \land ({(F \circ G) ↾}_{t}) {Isom}_{<, <^{-1}} (t, (F \circ G) [t]))) \to \exists s \in 𝒫 A ((R \leq \|s\| \land ({F ↾}_{s}) {Isom}_{<, <} (s, F [s])) \lor (S \leq \|s\| \land ({F ↾}_{s}) {Isom}_{<, <^{-1}} (s, F [s]))))$
134	23 133	sylan2b	$⊢ (φ \land t \in 𝒫 (1 \dots N + 1)) \to (((R \leq \|t\| \land ({(F \circ G) ↾}_{t}) {Isom}_{<, <} (t, (F \circ G) [t])) \lor (S \leq \|t\| \land ({(F \circ G) ↾}_{t}) {Isom}_{<, <^{-1}} (t, (F \circ G) [t]))) \to \exists s \in 𝒫 A ((R \leq \|s\| \land ({F ↾}_{s}) {Isom}_{<, <} (s, F [s])) \lor (S \leq \|s\| \land ({F ↾}_{s}) {Isom}_{<, <^{-1}} (s, F [s]))))$
135	134	rexlimdva	$⊢ φ \to (\exists t \in 𝒫 (1 \dots N + 1) ((R \leq \|t\| \land ({(F \circ G) ↾}_{t}) {Isom}_{<, <} (t, (F \circ G) [t])) \lor (S \leq \|t\| \land ({(F \circ G) ↾}_{t}) {Isom}_{<, <^{-1}} (t, (F \circ G) [t]))) \to \exists s \in 𝒫 A ((R \leq \|s\| \land ({F ↾}_{s}) {Isom}_{<, <} (s, F [s])) \lor (S \leq \|s\| \land ({F ↾}_{s}) {Isom}_{<, <^{-1}} (s, F [s]))))$
136	22 135	mpd	$⊢ φ \to \exists s \in 𝒫 A ((R \leq \|s\| \land ({F ↾}_{s}) {Isom}_{<, <} (s, F [s])) \lor (S \leq \|s\| \land ({F ↾}_{s}) {Isom}_{<, <^{-1}} (s, F [s])))$

Metamath Proof Explorer

Theorem erdsze2lem2

Proof