MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  f1otrg Structured version   Visualization version   GIF version

Theorem f1otrg 28669
Description: A bijection between bases which conserves distances and intervals conserves also geometries. (Contributed by Thierry Arnoux, 23-Mar-2019.)
Hypotheses
Ref Expression
f1otrkg.p 𝑃 = (Base‘𝐺)
f1otrkg.d 𝐷 = (dist‘𝐺)
f1otrkg.i 𝐼 = (Itv‘𝐺)
f1otrkg.b 𝐵 = (Base‘𝐻)
f1otrkg.e 𝐸 = (dist‘𝐻)
f1otrkg.j 𝐽 = (Itv‘𝐻)
f1otrkg.f (𝜑𝐹:𝐵1-1-onto𝑃)
f1otrkg.1 ((𝜑 ∧ (𝑒𝐵𝑓𝐵)) → (𝑒𝐸𝑓) = ((𝐹𝑒)𝐷(𝐹𝑓)))
f1otrkg.2 ((𝜑 ∧ (𝑒𝐵𝑓𝐵𝑔𝐵)) → (𝑔 ∈ (𝑒𝐽𝑓) ↔ (𝐹𝑔) ∈ ((𝐹𝑒)𝐼(𝐹𝑓))))
f1otrg.h (𝜑𝐻𝑉)
f1otrg.g (𝜑𝐺 ∈ TarskiG)
f1otrg.l (𝜑 → (LineG‘𝐻) = (𝑥𝐵, 𝑦 ∈ (𝐵 ∖ {𝑥}) ↦ {𝑧𝐵 ∣ (𝑧 ∈ (𝑥𝐽𝑦) ∨ 𝑥 ∈ (𝑧𝐽𝑦) ∨ 𝑦 ∈ (𝑥𝐽𝑧))}))
Assertion
Ref Expression
f1otrg (𝜑𝐻 ∈ TarskiG)
Distinct variable groups:   𝑒,𝑓,𝑔,𝑥,𝑦,𝑧,𝐵   𝐷,𝑒,𝑓,𝑔   𝑒,𝐸,𝑓,𝑔,𝑥,𝑦,𝑧   𝑒,𝐹,𝑓,𝑔,𝑥,𝑦,𝑧   𝑒,𝐼,𝑓,𝑔,𝑥,𝑦   𝑒,𝐽,𝑓,𝑔,𝑥,𝑦,𝑧   𝑃,𝑒,𝑓,𝑔,𝑥,𝑦,𝑧   𝜑,𝑒,𝑓,𝑔,𝑥,𝑦,𝑧   𝑓,𝐻
Allowed substitution hints:   𝐷(𝑥,𝑦,𝑧)   𝐺(𝑥,𝑦,𝑧,𝑒,𝑓,𝑔)   𝐻(𝑥,𝑦,𝑧,𝑒,𝑔)   𝐼(𝑧)   𝑉(𝑥,𝑦,𝑧,𝑒,𝑓,𝑔)

Proof of Theorem f1otrg
Dummy variables 𝑎 𝑏 𝑐 𝑖 𝑝 𝑠 𝑡 𝑢 𝑣 𝑤 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 f1otrg.h . . . . . 6 (𝜑𝐻𝑉)
21elexd 3491 . . . . 5 (𝜑𝐻 ∈ V)
3 f1otrkg.p . . . . . . . . 9 𝑃 = (Base‘𝐺)
4 f1otrkg.d . . . . . . . . 9 𝐷 = (dist‘𝐺)
5 f1otrkg.i . . . . . . . . 9 𝐼 = (Itv‘𝐺)
6 f1otrg.g . . . . . . . . . 10 (𝜑𝐺 ∈ TarskiG)
76adantr 480 . . . . . . . . 9 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → 𝐺 ∈ TarskiG)
8 f1otrkg.f . . . . . . . . . . . 12 (𝜑𝐹:𝐵1-1-onto𝑃)
9 f1of 6834 . . . . . . . . . . . 12 (𝐹:𝐵1-1-onto𝑃𝐹:𝐵𝑃)
108, 9syl 17 . . . . . . . . . . 11 (𝜑𝐹:𝐵𝑃)
1110adantr 480 . . . . . . . . . 10 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → 𝐹:𝐵𝑃)
12 simprl 770 . . . . . . . . . 10 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → 𝑥𝐵)
1311, 12ffvelcdmd 7090 . . . . . . . . 9 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → (𝐹𝑥) ∈ 𝑃)
14 simprr 772 . . . . . . . . . 10 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → 𝑦𝐵)
1511, 14ffvelcdmd 7090 . . . . . . . . 9 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → (𝐹𝑦) ∈ 𝑃)
163, 4, 5, 7, 13, 15axtgcgrrflx 28260 . . . . . . . 8 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → ((𝐹𝑥)𝐷(𝐹𝑦)) = ((𝐹𝑦)𝐷(𝐹𝑥)))
17 f1otrkg.b . . . . . . . . 9 𝐵 = (Base‘𝐻)
18 f1otrkg.e . . . . . . . . 9 𝐸 = (dist‘𝐻)
19 f1otrkg.j . . . . . . . . 9 𝐽 = (Itv‘𝐻)
208adantr 480 . . . . . . . . 9 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → 𝐹:𝐵1-1-onto𝑃)
21 f1otrkg.1 . . . . . . . . . 10 ((𝜑 ∧ (𝑒𝐵𝑓𝐵)) → (𝑒𝐸𝑓) = ((𝐹𝑒)𝐷(𝐹𝑓)))
2221adantlr 714 . . . . . . . . 9 (((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑒𝐵𝑓𝐵)) → (𝑒𝐸𝑓) = ((𝐹𝑒)𝐷(𝐹𝑓)))
23 f1otrkg.2 . . . . . . . . . 10 ((𝜑 ∧ (𝑒𝐵𝑓𝐵𝑔𝐵)) → (𝑔 ∈ (𝑒𝐽𝑓) ↔ (𝐹𝑔) ∈ ((𝐹𝑒)𝐼(𝐹𝑓))))
2423adantlr 714 . . . . . . . . 9 (((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑒𝐵𝑓𝐵𝑔𝐵)) → (𝑔 ∈ (𝑒𝐽𝑓) ↔ (𝐹𝑔) ∈ ((𝐹𝑒)𝐼(𝐹𝑓))))
253, 4, 5, 17, 18, 19, 20, 22, 24, 12, 14f1otrgds 28667 . . . . . . . 8 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → (𝑥𝐸𝑦) = ((𝐹𝑥)𝐷(𝐹𝑦)))
263, 4, 5, 17, 18, 19, 20, 22, 24, 14, 12f1otrgds 28667 . . . . . . . 8 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → (𝑦𝐸𝑥) = ((𝐹𝑦)𝐷(𝐹𝑥)))
2716, 25, 263eqtr4d 2778 . . . . . . 7 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → (𝑥𝐸𝑦) = (𝑦𝐸𝑥))
2827ralrimivva 3196 . . . . . 6 (𝜑 → ∀𝑥𝐵𝑦𝐵 (𝑥𝐸𝑦) = (𝑦𝐸𝑥))
29 f1of1 6833 . . . . . . . . . . 11 (𝐹:𝐵1-1-onto𝑃𝐹:𝐵1-1𝑃)
308, 29syl 17 . . . . . . . . . 10 (𝜑𝐹:𝐵1-1𝑃)
31303ad2ant1 1131 . . . . . . . . 9 ((𝜑 ∧ (𝑥𝐵𝑦𝐵𝑧𝐵) ∧ (𝑥𝐸𝑦) = (𝑧𝐸𝑧)) → 𝐹:𝐵1-1𝑃)
32 simp21 1204 . . . . . . . . . 10 ((𝜑 ∧ (𝑥𝐵𝑦𝐵𝑧𝐵) ∧ (𝑥𝐸𝑦) = (𝑧𝐸𝑧)) → 𝑥𝐵)
33 simp22 1205 . . . . . . . . . 10 ((𝜑 ∧ (𝑥𝐵𝑦𝐵𝑧𝐵) ∧ (𝑥𝐸𝑦) = (𝑧𝐸𝑧)) → 𝑦𝐵)
3432, 33jca 511 . . . . . . . . 9 ((𝜑 ∧ (𝑥𝐵𝑦𝐵𝑧𝐵) ∧ (𝑥𝐸𝑦) = (𝑧𝐸𝑧)) → (𝑥𝐵𝑦𝐵))
3563ad2ant1 1131 . . . . . . . . . 10 ((𝜑 ∧ (𝑥𝐵𝑦𝐵𝑧𝐵) ∧ (𝑥𝐸𝑦) = (𝑧𝐸𝑧)) → 𝐺 ∈ TarskiG)
36103ad2ant1 1131 . . . . . . . . . . 11 ((𝜑 ∧ (𝑥𝐵𝑦𝐵𝑧𝐵) ∧ (𝑥𝐸𝑦) = (𝑧𝐸𝑧)) → 𝐹:𝐵𝑃)
3736, 32ffvelcdmd 7090 . . . . . . . . . 10 ((𝜑 ∧ (𝑥𝐵𝑦𝐵𝑧𝐵) ∧ (𝑥𝐸𝑦) = (𝑧𝐸𝑧)) → (𝐹𝑥) ∈ 𝑃)
3836, 33ffvelcdmd 7090 . . . . . . . . . 10 ((𝜑 ∧ (𝑥𝐵𝑦𝐵𝑧𝐵) ∧ (𝑥𝐸𝑦) = (𝑧𝐸𝑧)) → (𝐹𝑦) ∈ 𝑃)
39 simp23 1206 . . . . . . . . . . 11 ((𝜑 ∧ (𝑥𝐵𝑦𝐵𝑧𝐵) ∧ (𝑥𝐸𝑦) = (𝑧𝐸𝑧)) → 𝑧𝐵)
4036, 39ffvelcdmd 7090 . . . . . . . . . 10 ((𝜑 ∧ (𝑥𝐵𝑦𝐵𝑧𝐵) ∧ (𝑥𝐸𝑦) = (𝑧𝐸𝑧)) → (𝐹𝑧) ∈ 𝑃)
41 simp3 1136 . . . . . . . . . . 11 ((𝜑 ∧ (𝑥𝐵𝑦𝐵𝑧𝐵) ∧ (𝑥𝐸𝑦) = (𝑧𝐸𝑧)) → (𝑥𝐸𝑦) = (𝑧𝐸𝑧))
4283ad2ant1 1131 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑥𝐵𝑦𝐵𝑧𝐵) ∧ (𝑥𝐸𝑦) = (𝑧𝐸𝑧)) → 𝐹:𝐵1-1-onto𝑃)
43213ad2antl1 1183 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑥𝐵𝑦𝐵𝑧𝐵) ∧ (𝑥𝐸𝑦) = (𝑧𝐸𝑧)) ∧ (𝑒𝐵𝑓𝐵)) → (𝑒𝐸𝑓) = ((𝐹𝑒)𝐷(𝐹𝑓)))
44233ad2antl1 1183 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑥𝐵𝑦𝐵𝑧𝐵) ∧ (𝑥𝐸𝑦) = (𝑧𝐸𝑧)) ∧ (𝑒𝐵𝑓𝐵𝑔𝐵)) → (𝑔 ∈ (𝑒𝐽𝑓) ↔ (𝐹𝑔) ∈ ((𝐹𝑒)𝐼(𝐹𝑓))))
453, 4, 5, 17, 18, 19, 42, 43, 44, 32, 33f1otrgds 28667 . . . . . . . . . . 11 ((𝜑 ∧ (𝑥𝐵𝑦𝐵𝑧𝐵) ∧ (𝑥𝐸𝑦) = (𝑧𝐸𝑧)) → (𝑥𝐸𝑦) = ((𝐹𝑥)𝐷(𝐹𝑦)))
463, 4, 5, 17, 18, 19, 42, 43, 44, 39, 39f1otrgds 28667 . . . . . . . . . . 11 ((𝜑 ∧ (𝑥𝐵𝑦𝐵𝑧𝐵) ∧ (𝑥𝐸𝑦) = (𝑧𝐸𝑧)) → (𝑧𝐸𝑧) = ((𝐹𝑧)𝐷(𝐹𝑧)))
4741, 45, 463eqtr3d 2776 . . . . . . . . . 10 ((𝜑 ∧ (𝑥𝐵𝑦𝐵𝑧𝐵) ∧ (𝑥𝐸𝑦) = (𝑧𝐸𝑧)) → ((𝐹𝑥)𝐷(𝐹𝑦)) = ((𝐹𝑧)𝐷(𝐹𝑧)))
483, 4, 5, 35, 37, 38, 40, 47axtgcgrid 28261 . . . . . . . . 9 ((𝜑 ∧ (𝑥𝐵𝑦𝐵𝑧𝐵) ∧ (𝑥𝐸𝑦) = (𝑧𝐸𝑧)) → (𝐹𝑥) = (𝐹𝑦))
49 f1veqaeq 7262 . . . . . . . . . 10 ((𝐹:𝐵1-1𝑃 ∧ (𝑥𝐵𝑦𝐵)) → ((𝐹𝑥) = (𝐹𝑦) → 𝑥 = 𝑦))
5049imp 406 . . . . . . . . 9 (((𝐹:𝐵1-1𝑃 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝐹𝑥) = (𝐹𝑦)) → 𝑥 = 𝑦)
5131, 34, 48, 50syl21anc 837 . . . . . . . 8 ((𝜑 ∧ (𝑥𝐵𝑦𝐵𝑧𝐵) ∧ (𝑥𝐸𝑦) = (𝑧𝐸𝑧)) → 𝑥 = 𝑦)
52513expia 1119 . . . . . . 7 ((𝜑 ∧ (𝑥𝐵𝑦𝐵𝑧𝐵)) → ((𝑥𝐸𝑦) = (𝑧𝐸𝑧) → 𝑥 = 𝑦))
5352ralrimivvva 3199 . . . . . 6 (𝜑 → ∀𝑥𝐵𝑦𝐵𝑧𝐵 ((𝑥𝐸𝑦) = (𝑧𝐸𝑧) → 𝑥 = 𝑦))
5428, 53jca 511 . . . . 5 (𝜑 → (∀𝑥𝐵𝑦𝐵 (𝑥𝐸𝑦) = (𝑦𝐸𝑥) ∧ ∀𝑥𝐵𝑦𝐵𝑧𝐵 ((𝑥𝐸𝑦) = (𝑧𝐸𝑧) → 𝑥 = 𝑦)))
5517, 18, 19istrkgc 28252 . . . . 5 (𝐻 ∈ TarskiGC ↔ (𝐻 ∈ V ∧ (∀𝑥𝐵𝑦𝐵 (𝑥𝐸𝑦) = (𝑦𝐸𝑥) ∧ ∀𝑥𝐵𝑦𝐵𝑧𝐵 ((𝑥𝐸𝑦) = (𝑧𝐸𝑧) → 𝑥 = 𝑦))))
562, 54, 55sylanbrc 582 . . . 4 (𝜑𝐻 ∈ TarskiGC)
5783ad2ant1 1131 . . . . . . . . . 10 ((𝜑 ∧ (𝑥𝐵𝑦𝐵) ∧ 𝑦 ∈ (𝑥𝐽𝑥)) → 𝐹:𝐵1-1-onto𝑃)
5857, 29syl 17 . . . . . . . . 9 ((𝜑 ∧ (𝑥𝐵𝑦𝐵) ∧ 𝑦 ∈ (𝑥𝐽𝑥)) → 𝐹:𝐵1-1𝑃)
59 simp2 1135 . . . . . . . . 9 ((𝜑 ∧ (𝑥𝐵𝑦𝐵) ∧ 𝑦 ∈ (𝑥𝐽𝑥)) → (𝑥𝐵𝑦𝐵))
6063ad2ant1 1131 . . . . . . . . . 10 ((𝜑 ∧ (𝑥𝐵𝑦𝐵) ∧ 𝑦 ∈ (𝑥𝐽𝑥)) → 𝐺 ∈ TarskiG)
61133adant3 1130 . . . . . . . . . 10 ((𝜑 ∧ (𝑥𝐵𝑦𝐵) ∧ 𝑦 ∈ (𝑥𝐽𝑥)) → (𝐹𝑥) ∈ 𝑃)
62153adant3 1130 . . . . . . . . . 10 ((𝜑 ∧ (𝑥𝐵𝑦𝐵) ∧ 𝑦 ∈ (𝑥𝐽𝑥)) → (𝐹𝑦) ∈ 𝑃)
63 simp3 1136 . . . . . . . . . . 11 ((𝜑 ∧ (𝑥𝐵𝑦𝐵) ∧ 𝑦 ∈ (𝑥𝐽𝑥)) → 𝑦 ∈ (𝑥𝐽𝑥))
64213ad2antl1 1183 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑥𝐵𝑦𝐵) ∧ 𝑦 ∈ (𝑥𝐽𝑥)) ∧ (𝑒𝐵𝑓𝐵)) → (𝑒𝐸𝑓) = ((𝐹𝑒)𝐷(𝐹𝑓)))
65233ad2antl1 1183 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑥𝐵𝑦𝐵) ∧ 𝑦 ∈ (𝑥𝐽𝑥)) ∧ (𝑒𝐵𝑓𝐵𝑔𝐵)) → (𝑔 ∈ (𝑒𝐽𝑓) ↔ (𝐹𝑔) ∈ ((𝐹𝑒)𝐼(𝐹𝑓))))
66123adant3 1130 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑥𝐵𝑦𝐵) ∧ 𝑦 ∈ (𝑥𝐽𝑥)) → 𝑥𝐵)
67143adant3 1130 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑥𝐵𝑦𝐵) ∧ 𝑦 ∈ (𝑥𝐽𝑥)) → 𝑦𝐵)
683, 4, 5, 17, 18, 19, 57, 64, 65, 66, 66, 67f1otrgitv 28668 . . . . . . . . . . 11 ((𝜑 ∧ (𝑥𝐵𝑦𝐵) ∧ 𝑦 ∈ (𝑥𝐽𝑥)) → (𝑦 ∈ (𝑥𝐽𝑥) ↔ (𝐹𝑦) ∈ ((𝐹𝑥)𝐼(𝐹𝑥))))
6963, 68mpbid 231 . . . . . . . . . 10 ((𝜑 ∧ (𝑥𝐵𝑦𝐵) ∧ 𝑦 ∈ (𝑥𝐽𝑥)) → (𝐹𝑦) ∈ ((𝐹𝑥)𝐼(𝐹𝑥)))
703, 4, 5, 60, 61, 62, 69axtgbtwnid 28264 . . . . . . . . 9 ((𝜑 ∧ (𝑥𝐵𝑦𝐵) ∧ 𝑦 ∈ (𝑥𝐽𝑥)) → (𝐹𝑥) = (𝐹𝑦))
7158, 59, 70, 50syl21anc 837 . . . . . . . 8 ((𝜑 ∧ (𝑥𝐵𝑦𝐵) ∧ 𝑦 ∈ (𝑥𝐽𝑥)) → 𝑥 = 𝑦)
72713expia 1119 . . . . . . 7 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → (𝑦 ∈ (𝑥𝐽𝑥) → 𝑥 = 𝑦))
7372ralrimivva 3196 . . . . . 6 (𝜑 → ∀𝑥𝐵𝑦𝐵 (𝑦 ∈ (𝑥𝐽𝑥) → 𝑥 = 𝑦))
74 f1ocnv 6846 . . . . . . . . . . . . . 14 (𝐹:𝐵1-1-onto𝑃𝐹:𝑃1-1-onto𝐵)
75 f1of 6834 . . . . . . . . . . . . . 14 (𝐹:𝑃1-1-onto𝐵𝐹:𝑃𝐵)
768, 74, 753syl 18 . . . . . . . . . . . . 13 (𝜑𝐹:𝑃𝐵)
7776ad5antr 733 . . . . . . . . . . . 12 ((((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐𝑃) ∧ (𝑐 ∈ ((𝐹𝑢)𝐼(𝐹𝑦)) ∧ 𝑐 ∈ ((𝐹𝑣)𝐼(𝐹𝑥)))) → 𝐹:𝑃𝐵)
78 simplr 768 . . . . . . . . . . . 12 ((((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐𝑃) ∧ (𝑐 ∈ ((𝐹𝑢)𝐼(𝐹𝑦)) ∧ 𝑐 ∈ ((𝐹𝑣)𝐼(𝐹𝑥)))) → 𝑐𝑃)
7977, 78ffvelcdmd 7090 . . . . . . . . . . 11 ((((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐𝑃) ∧ (𝑐 ∈ ((𝐹𝑢)𝐼(𝐹𝑦)) ∧ 𝑐 ∈ ((𝐹𝑣)𝐼(𝐹𝑥)))) → (𝐹𝑐) ∈ 𝐵)
80 simpr 484 . . . . . . . . . . . . 13 (((((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐𝑃) ∧ (𝑐 ∈ ((𝐹𝑢)𝐼(𝐹𝑦)) ∧ 𝑐 ∈ ((𝐹𝑣)𝐼(𝐹𝑥)))) ∧ 𝑎 = (𝐹𝑐)) → 𝑎 = (𝐹𝑐))
8180eleq1d 2814 . . . . . . . . . . . 12 (((((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐𝑃) ∧ (𝑐 ∈ ((𝐹𝑢)𝐼(𝐹𝑦)) ∧ 𝑐 ∈ ((𝐹𝑣)𝐼(𝐹𝑥)))) ∧ 𝑎 = (𝐹𝑐)) → (𝑎 ∈ (𝑢𝐽𝑦) ↔ (𝐹𝑐) ∈ (𝑢𝐽𝑦)))
8280eleq1d 2814 . . . . . . . . . . . 12 (((((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐𝑃) ∧ (𝑐 ∈ ((𝐹𝑢)𝐼(𝐹𝑦)) ∧ 𝑐 ∈ ((𝐹𝑣)𝐼(𝐹𝑥)))) ∧ 𝑎 = (𝐹𝑐)) → (𝑎 ∈ (𝑣𝐽𝑥) ↔ (𝐹𝑐) ∈ (𝑣𝐽𝑥)))
8381, 82anbi12d 631 . . . . . . . . . . 11 (((((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐𝑃) ∧ (𝑐 ∈ ((𝐹𝑢)𝐼(𝐹𝑦)) ∧ 𝑐 ∈ ((𝐹𝑣)𝐼(𝐹𝑥)))) ∧ 𝑎 = (𝐹𝑐)) → ((𝑎 ∈ (𝑢𝐽𝑦) ∧ 𝑎 ∈ (𝑣𝐽𝑥)) ↔ ((𝐹𝑐) ∈ (𝑢𝐽𝑦) ∧ (𝐹𝑐) ∈ (𝑣𝐽𝑥))))
84 simprl 770 . . . . . . . . . . . . . 14 ((((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐𝑃) ∧ (𝑐 ∈ ((𝐹𝑢)𝐼(𝐹𝑦)) ∧ 𝑐 ∈ ((𝐹𝑣)𝐼(𝐹𝑥)))) → 𝑐 ∈ ((𝐹𝑢)𝐼(𝐹𝑦)))
8520ad2antrr 725 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) → 𝐹:𝐵1-1-onto𝑃)
8685ad2antrr 725 . . . . . . . . . . . . . . 15 ((((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐𝑃) ∧ (𝑐 ∈ ((𝐹𝑢)𝐼(𝐹𝑦)) ∧ 𝑐 ∈ ((𝐹𝑣)𝐼(𝐹𝑥)))) → 𝐹:𝐵1-1-onto𝑃)
87 f1ocnvfv2 7281 . . . . . . . . . . . . . . . 16 ((𝐹:𝐵1-1-onto𝑃𝑐𝑃) → (𝐹‘(𝐹𝑐)) = 𝑐)
8887eleq1d 2814 . . . . . . . . . . . . . . 15 ((𝐹:𝐵1-1-onto𝑃𝑐𝑃) → ((𝐹‘(𝐹𝑐)) ∈ ((𝐹𝑢)𝐼(𝐹𝑦)) ↔ 𝑐 ∈ ((𝐹𝑢)𝐼(𝐹𝑦))))
8986, 78, 88syl2anc 583 . . . . . . . . . . . . . 14 ((((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐𝑃) ∧ (𝑐 ∈ ((𝐹𝑢)𝐼(𝐹𝑦)) ∧ 𝑐 ∈ ((𝐹𝑣)𝐼(𝐹𝑥)))) → ((𝐹‘(𝐹𝑐)) ∈ ((𝐹𝑢)𝐼(𝐹𝑦)) ↔ 𝑐 ∈ ((𝐹𝑢)𝐼(𝐹𝑦))))
9084, 89mpbird 257 . . . . . . . . . . . . 13 ((((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐𝑃) ∧ (𝑐 ∈ ((𝐹𝑢)𝐼(𝐹𝑦)) ∧ 𝑐 ∈ ((𝐹𝑣)𝐼(𝐹𝑥)))) → (𝐹‘(𝐹𝑐)) ∈ ((𝐹𝑢)𝐼(𝐹𝑦)))
9122ad4ant14 751 . . . . . . . . . . . . . . 15 (((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ (𝑒𝐵𝑓𝐵)) → (𝑒𝐸𝑓) = ((𝐹𝑒)𝐷(𝐹𝑓)))
9291ad4ant14 751 . . . . . . . . . . . . . 14 (((((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐𝑃) ∧ (𝑐 ∈ ((𝐹𝑢)𝐼(𝐹𝑦)) ∧ 𝑐 ∈ ((𝐹𝑣)𝐼(𝐹𝑥)))) ∧ (𝑒𝐵𝑓𝐵)) → (𝑒𝐸𝑓) = ((𝐹𝑒)𝐷(𝐹𝑓)))
9324ad4ant14 751 . . . . . . . . . . . . . . 15 (((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ (𝑒𝐵𝑓𝐵𝑔𝐵)) → (𝑔 ∈ (𝑒𝐽𝑓) ↔ (𝐹𝑔) ∈ ((𝐹𝑒)𝐼(𝐹𝑓))))
9493ad4ant14 751 . . . . . . . . . . . . . 14 (((((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐𝑃) ∧ (𝑐 ∈ ((𝐹𝑢)𝐼(𝐹𝑦)) ∧ 𝑐 ∈ ((𝐹𝑣)𝐼(𝐹𝑥)))) ∧ (𝑒𝐵𝑓𝐵𝑔𝐵)) → (𝑔 ∈ (𝑒𝐽𝑓) ↔ (𝐹𝑔) ∈ ((𝐹𝑒)𝐼(𝐹𝑓))))
95 simplr2 1214 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) → 𝑢𝐵)
9695ad2antrr 725 . . . . . . . . . . . . . 14 ((((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐𝑃) ∧ (𝑐 ∈ ((𝐹𝑢)𝐼(𝐹𝑦)) ∧ 𝑐 ∈ ((𝐹𝑣)𝐼(𝐹𝑥)))) → 𝑢𝐵)
9714ad2antrr 725 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) → 𝑦𝐵)
9897ad2antrr 725 . . . . . . . . . . . . . 14 ((((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐𝑃) ∧ (𝑐 ∈ ((𝐹𝑢)𝐼(𝐹𝑦)) ∧ 𝑐 ∈ ((𝐹𝑣)𝐼(𝐹𝑥)))) → 𝑦𝐵)
993, 4, 5, 17, 18, 19, 86, 92, 94, 96, 98, 79f1otrgitv 28668 . . . . . . . . . . . . 13 ((((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐𝑃) ∧ (𝑐 ∈ ((𝐹𝑢)𝐼(𝐹𝑦)) ∧ 𝑐 ∈ ((𝐹𝑣)𝐼(𝐹𝑥)))) → ((𝐹𝑐) ∈ (𝑢𝐽𝑦) ↔ (𝐹‘(𝐹𝑐)) ∈ ((𝐹𝑢)𝐼(𝐹𝑦))))
10090, 99mpbird 257 . . . . . . . . . . . 12 ((((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐𝑃) ∧ (𝑐 ∈ ((𝐹𝑢)𝐼(𝐹𝑦)) ∧ 𝑐 ∈ ((𝐹𝑣)𝐼(𝐹𝑥)))) → (𝐹𝑐) ∈ (𝑢𝐽𝑦))
101 simprr 772 . . . . . . . . . . . . . 14 ((((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐𝑃) ∧ (𝑐 ∈ ((𝐹𝑢)𝐼(𝐹𝑦)) ∧ 𝑐 ∈ ((𝐹𝑣)𝐼(𝐹𝑥)))) → 𝑐 ∈ ((𝐹𝑣)𝐼(𝐹𝑥)))
10287eleq1d 2814 . . . . . . . . . . . . . . 15 ((𝐹:𝐵1-1-onto𝑃𝑐𝑃) → ((𝐹‘(𝐹𝑐)) ∈ ((𝐹𝑣)𝐼(𝐹𝑥)) ↔ 𝑐 ∈ ((𝐹𝑣)𝐼(𝐹𝑥))))
10386, 78, 102syl2anc 583 . . . . . . . . . . . . . 14 ((((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐𝑃) ∧ (𝑐 ∈ ((𝐹𝑢)𝐼(𝐹𝑦)) ∧ 𝑐 ∈ ((𝐹𝑣)𝐼(𝐹𝑥)))) → ((𝐹‘(𝐹𝑐)) ∈ ((𝐹𝑣)𝐼(𝐹𝑥)) ↔ 𝑐 ∈ ((𝐹𝑣)𝐼(𝐹𝑥))))
104101, 103mpbird 257 . . . . . . . . . . . . 13 ((((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐𝑃) ∧ (𝑐 ∈ ((𝐹𝑢)𝐼(𝐹𝑦)) ∧ 𝑐 ∈ ((𝐹𝑣)𝐼(𝐹𝑥)))) → (𝐹‘(𝐹𝑐)) ∈ ((𝐹𝑣)𝐼(𝐹𝑥)))
105 simplr3 1215 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) → 𝑣𝐵)
106105ad2antrr 725 . . . . . . . . . . . . . 14 ((((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐𝑃) ∧ (𝑐 ∈ ((𝐹𝑢)𝐼(𝐹𝑦)) ∧ 𝑐 ∈ ((𝐹𝑣)𝐼(𝐹𝑥)))) → 𝑣𝐵)
10712ad2antrr 725 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) → 𝑥𝐵)
108107ad2antrr 725 . . . . . . . . . . . . . 14 ((((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐𝑃) ∧ (𝑐 ∈ ((𝐹𝑢)𝐼(𝐹𝑦)) ∧ 𝑐 ∈ ((𝐹𝑣)𝐼(𝐹𝑥)))) → 𝑥𝐵)
1093, 4, 5, 17, 18, 19, 86, 92, 94, 106, 108, 79f1otrgitv 28668 . . . . . . . . . . . . 13 ((((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐𝑃) ∧ (𝑐 ∈ ((𝐹𝑢)𝐼(𝐹𝑦)) ∧ 𝑐 ∈ ((𝐹𝑣)𝐼(𝐹𝑥)))) → ((𝐹𝑐) ∈ (𝑣𝐽𝑥) ↔ (𝐹‘(𝐹𝑐)) ∈ ((𝐹𝑣)𝐼(𝐹𝑥))))
110104, 109mpbird 257 . . . . . . . . . . . 12 ((((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐𝑃) ∧ (𝑐 ∈ ((𝐹𝑢)𝐼(𝐹𝑦)) ∧ 𝑐 ∈ ((𝐹𝑣)𝐼(𝐹𝑥)))) → (𝐹𝑐) ∈ (𝑣𝐽𝑥))
111100, 110jca 511 . . . . . . . . . . 11 ((((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐𝑃) ∧ (𝑐 ∈ ((𝐹𝑢)𝐼(𝐹𝑦)) ∧ 𝑐 ∈ ((𝐹𝑣)𝐼(𝐹𝑥)))) → ((𝐹𝑐) ∈ (𝑢𝐽𝑦) ∧ (𝐹𝑐) ∈ (𝑣𝐽𝑥)))
11279, 83, 111rspcedvd 3610 . . . . . . . . . 10 ((((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐𝑃) ∧ (𝑐 ∈ ((𝐹𝑢)𝐼(𝐹𝑦)) ∧ 𝑐 ∈ ((𝐹𝑣)𝐼(𝐹𝑥)))) → ∃𝑎𝐵 (𝑎 ∈ (𝑢𝐽𝑦) ∧ 𝑎 ∈ (𝑣𝐽𝑥)))
1137ad2antrr 725 . . . . . . . . . . 11 ((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) → 𝐺 ∈ TarskiG)
11411ad2antrr 725 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) → 𝐹:𝐵𝑃)
115114, 107ffvelcdmd 7090 . . . . . . . . . . 11 ((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) → (𝐹𝑥) ∈ 𝑃)
116114, 97ffvelcdmd 7090 . . . . . . . . . . 11 ((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) → (𝐹𝑦) ∈ 𝑃)
117 simplr1 1213 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) → 𝑧𝐵)
118114, 117ffvelcdmd 7090 . . . . . . . . . . 11 ((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) → (𝐹𝑧) ∈ 𝑃)
119114, 95ffvelcdmd 7090 . . . . . . . . . . 11 ((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) → (𝐹𝑢) ∈ 𝑃)
120114, 105ffvelcdmd 7090 . . . . . . . . . . 11 ((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) → (𝐹𝑣) ∈ 𝑃)
121 simprl 770 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) → 𝑢 ∈ (𝑥𝐽𝑧))
1223, 4, 5, 17, 18, 19, 85, 91, 93, 107, 117, 95f1otrgitv 28668 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) → (𝑢 ∈ (𝑥𝐽𝑧) ↔ (𝐹𝑢) ∈ ((𝐹𝑥)𝐼(𝐹𝑧))))
123121, 122mpbid 231 . . . . . . . . . . 11 ((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) → (𝐹𝑢) ∈ ((𝐹𝑥)𝐼(𝐹𝑧)))
124 simprr 772 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) → 𝑣 ∈ (𝑦𝐽𝑧))
1253, 4, 5, 17, 18, 19, 85, 91, 93, 97, 117, 105f1otrgitv 28668 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) → (𝑣 ∈ (𝑦𝐽𝑧) ↔ (𝐹𝑣) ∈ ((𝐹𝑦)𝐼(𝐹𝑧))))
126124, 125mpbid 231 . . . . . . . . . . 11 ((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) → (𝐹𝑣) ∈ ((𝐹𝑦)𝐼(𝐹𝑧)))
1273, 4, 5, 113, 115, 116, 118, 119, 120, 123, 126axtgpasch 28265 . . . . . . . . . 10 ((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) → ∃𝑐𝑃 (𝑐 ∈ ((𝐹𝑢)𝐼(𝐹𝑦)) ∧ 𝑐 ∈ ((𝐹𝑣)𝐼(𝐹𝑥))))
128112, 127r19.29a 3158 . . . . . . . . 9 ((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) → ∃𝑎𝐵 (𝑎 ∈ (𝑢𝐽𝑦) ∧ 𝑎 ∈ (𝑣𝐽𝑥)))
129128ex 412 . . . . . . . 8 (((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) → ((𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧)) → ∃𝑎𝐵 (𝑎 ∈ (𝑢𝐽𝑦) ∧ 𝑎 ∈ (𝑣𝐽𝑥))))
130129ralrimivvva 3199 . . . . . . 7 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → ∀𝑧𝐵𝑢𝐵𝑣𝐵 ((𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧)) → ∃𝑎𝐵 (𝑎 ∈ (𝑢𝐽𝑦) ∧ 𝑎 ∈ (𝑣𝐽𝑥))))
131130ralrimivva 3196 . . . . . 6 (𝜑 → ∀𝑥𝐵𝑦𝐵𝑧𝐵𝑢𝐵𝑣𝐵 ((𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧)) → ∃𝑎𝐵 (𝑎 ∈ (𝑢𝐽𝑦) ∧ 𝑎 ∈ (𝑣𝐽𝑥))))
1328ad5antr 733 . . . . . . . . . . . . . . 15 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ 𝑐𝑃) ∧ ∀𝑒 ∈ (𝐹𝑠)∀𝑓 ∈ (𝐹𝑡)𝑐 ∈ (𝑒𝐼𝑓)) ∧ (𝑥𝑠𝑦𝑡)) → 𝐹:𝐵1-1-onto𝑃)
133 simpllr 775 . . . . . . . . . . . . . . 15 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ 𝑐𝑃) ∧ ∀𝑒 ∈ (𝐹𝑠)∀𝑓 ∈ (𝐹𝑡)𝑐 ∈ (𝑒𝐼𝑓)) ∧ (𝑥𝑠𝑦𝑡)) → 𝑐𝑃)
134132, 133, 87syl2anc 583 . . . . . . . . . . . . . 14 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ 𝑐𝑃) ∧ ∀𝑒 ∈ (𝐹𝑠)∀𝑓 ∈ (𝐹𝑡)𝑐 ∈ (𝑒𝐼𝑓)) ∧ (𝑥𝑠𝑦𝑡)) → (𝐹‘(𝐹𝑐)) = 𝑐)
135 ffn 6717 . . . . . . . . . . . . . . . . 17 (𝐹:𝐵𝑃𝐹 Fn 𝐵)
136132, 9, 1353syl 18 . . . . . . . . . . . . . . . 16 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ 𝑐𝑃) ∧ ∀𝑒 ∈ (𝐹𝑠)∀𝑓 ∈ (𝐹𝑡)𝑐 ∈ (𝑒𝐼𝑓)) ∧ (𝑥𝑠𝑦𝑡)) → 𝐹 Fn 𝐵)
137 simp-4r 783 . . . . . . . . . . . . . . . . . . 19 (((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ 𝑐𝑃) ∧ (𝑥𝑠𝑦𝑡)) → (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵))
138137simpld 494 . . . . . . . . . . . . . . . . . 18 (((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ 𝑐𝑃) ∧ (𝑥𝑠𝑦𝑡)) → 𝑠 ∈ 𝒫 𝐵)
139138elpwid 4608 . . . . . . . . . . . . . . . . 17 (((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ 𝑐𝑃) ∧ (𝑥𝑠𝑦𝑡)) → 𝑠𝐵)
140139adantlr 714 . . . . . . . . . . . . . . . 16 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ 𝑐𝑃) ∧ ∀𝑒 ∈ (𝐹𝑠)∀𝑓 ∈ (𝐹𝑡)𝑐 ∈ (𝑒𝐼𝑓)) ∧ (𝑥𝑠𝑦𝑡)) → 𝑠𝐵)
141 simprl 770 . . . . . . . . . . . . . . . 16 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ 𝑐𝑃) ∧ ∀𝑒 ∈ (𝐹𝑠)∀𝑓 ∈ (𝐹𝑡)𝑐 ∈ (𝑒𝐼𝑓)) ∧ (𝑥𝑠𝑦𝑡)) → 𝑥𝑠)
142 fnfvima 7240 . . . . . . . . . . . . . . . 16 ((𝐹 Fn 𝐵𝑠𝐵𝑥𝑠) → (𝐹𝑥) ∈ (𝐹𝑠))
143136, 140, 141, 142syl3anc 1369 . . . . . . . . . . . . . . 15 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ 𝑐𝑃) ∧ ∀𝑒 ∈ (𝐹𝑠)∀𝑓 ∈ (𝐹𝑡)𝑐 ∈ (𝑒𝐼𝑓)) ∧ (𝑥𝑠𝑦𝑡)) → (𝐹𝑥) ∈ (𝐹𝑠))
144137simprd 495 . . . . . . . . . . . . . . . . . 18 (((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ 𝑐𝑃) ∧ (𝑥𝑠𝑦𝑡)) → 𝑡 ∈ 𝒫 𝐵)
145144elpwid 4608 . . . . . . . . . . . . . . . . 17 (((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ 𝑐𝑃) ∧ (𝑥𝑠𝑦𝑡)) → 𝑡𝐵)
146145adantlr 714 . . . . . . . . . . . . . . . 16 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ 𝑐𝑃) ∧ ∀𝑒 ∈ (𝐹𝑠)∀𝑓 ∈ (𝐹𝑡)𝑐 ∈ (𝑒𝐼𝑓)) ∧ (𝑥𝑠𝑦𝑡)) → 𝑡𝐵)
147 simprr 772 . . . . . . . . . . . . . . . 16 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ 𝑐𝑃) ∧ ∀𝑒 ∈ (𝐹𝑠)∀𝑓 ∈ (𝐹𝑡)𝑐 ∈ (𝑒𝐼𝑓)) ∧ (𝑥𝑠𝑦𝑡)) → 𝑦𝑡)
148 fnfvima 7240 . . . . . . . . . . . . . . . 16 ((𝐹 Fn 𝐵𝑡𝐵𝑦𝑡) → (𝐹𝑦) ∈ (𝐹𝑡))
149136, 146, 147, 148syl3anc 1369 . . . . . . . . . . . . . . 15 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ 𝑐𝑃) ∧ ∀𝑒 ∈ (𝐹𝑠)∀𝑓 ∈ (𝐹𝑡)𝑐 ∈ (𝑒𝐼𝑓)) ∧ (𝑥𝑠𝑦𝑡)) → (𝐹𝑦) ∈ (𝐹𝑡))
150 simplr 768 . . . . . . . . . . . . . . 15 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ 𝑐𝑃) ∧ ∀𝑒 ∈ (𝐹𝑠)∀𝑓 ∈ (𝐹𝑡)𝑐 ∈ (𝑒𝐼𝑓)) ∧ (𝑥𝑠𝑦𝑡)) → ∀𝑒 ∈ (𝐹𝑠)∀𝑓 ∈ (𝐹𝑡)𝑐 ∈ (𝑒𝐼𝑓))
151 oveq1 7422 . . . . . . . . . . . . . . . . 17 (𝑒 = (𝐹𝑥) → (𝑒𝐼𝑓) = ((𝐹𝑥)𝐼𝑓))
152151eleq2d 2815 . . . . . . . . . . . . . . . 16 (𝑒 = (𝐹𝑥) → (𝑐 ∈ (𝑒𝐼𝑓) ↔ 𝑐 ∈ ((𝐹𝑥)𝐼𝑓)))
153 oveq2 7423 . . . . . . . . . . . . . . . . 17 (𝑓 = (𝐹𝑦) → ((𝐹𝑥)𝐼𝑓) = ((𝐹𝑥)𝐼(𝐹𝑦)))
154153eleq2d 2815 . . . . . . . . . . . . . . . 16 (𝑓 = (𝐹𝑦) → (𝑐 ∈ ((𝐹𝑥)𝐼𝑓) ↔ 𝑐 ∈ ((𝐹𝑥)𝐼(𝐹𝑦))))
155152, 154rspc2va 3620 . . . . . . . . . . . . . . 15 ((((𝐹𝑥) ∈ (𝐹𝑠) ∧ (𝐹𝑦) ∈ (𝐹𝑡)) ∧ ∀𝑒 ∈ (𝐹𝑠)∀𝑓 ∈ (𝐹𝑡)𝑐 ∈ (𝑒𝐼𝑓)) → 𝑐 ∈ ((𝐹𝑥)𝐼(𝐹𝑦)))
156143, 149, 150, 155syl21anc 837 . . . . . . . . . . . . . 14 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ 𝑐𝑃) ∧ ∀𝑒 ∈ (𝐹𝑠)∀𝑓 ∈ (𝐹𝑡)𝑐 ∈ (𝑒𝐼𝑓)) ∧ (𝑥𝑠𝑦𝑡)) → 𝑐 ∈ ((𝐹𝑥)𝐼(𝐹𝑦)))
157134, 156eqeltrd 2829 . . . . . . . . . . . . 13 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ 𝑐𝑃) ∧ ∀𝑒 ∈ (𝐹𝑠)∀𝑓 ∈ (𝐹𝑡)𝑐 ∈ (𝑒𝐼𝑓)) ∧ (𝑥𝑠𝑦𝑡)) → (𝐹‘(𝐹𝑐)) ∈ ((𝐹𝑥)𝐼(𝐹𝑦)))
1588ad4antr 731 . . . . . . . . . . . . . . 15 (((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ 𝑐𝑃) ∧ (𝑥𝑠𝑦𝑡)) → 𝐹:𝐵1-1-onto𝑃)
159 simp-5l 784 . . . . . . . . . . . . . . . 16 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ 𝑐𝑃) ∧ (𝑥𝑠𝑦𝑡)) ∧ (𝑒𝐵𝑓𝐵)) → 𝜑)
160159, 21sylancom 587 . . . . . . . . . . . . . . 15 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ 𝑐𝑃) ∧ (𝑥𝑠𝑦𝑡)) ∧ (𝑒𝐵𝑓𝐵)) → (𝑒𝐸𝑓) = ((𝐹𝑒)𝐷(𝐹𝑓)))
161 simp-5l 784 . . . . . . . . . . . . . . . 16 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ 𝑐𝑃) ∧ (𝑥𝑠𝑦𝑡)) ∧ (𝑒𝐵𝑓𝐵𝑔𝐵)) → 𝜑)
162161, 23sylancom 587 . . . . . . . . . . . . . . 15 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ 𝑐𝑃) ∧ (𝑥𝑠𝑦𝑡)) ∧ (𝑒𝐵𝑓𝐵𝑔𝐵)) → (𝑔 ∈ (𝑒𝐽𝑓) ↔ (𝐹𝑔) ∈ ((𝐹𝑒)𝐼(𝐹𝑓))))
163 simprl 770 . . . . . . . . . . . . . . . 16 (((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ 𝑐𝑃) ∧ (𝑥𝑠𝑦𝑡)) → 𝑥𝑠)
164139, 163sseldd 3980 . . . . . . . . . . . . . . 15 (((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ 𝑐𝑃) ∧ (𝑥𝑠𝑦𝑡)) → 𝑥𝐵)
165 simprr 772 . . . . . . . . . . . . . . . 16 (((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ 𝑐𝑃) ∧ (𝑥𝑠𝑦𝑡)) → 𝑦𝑡)
166145, 165sseldd 3980 . . . . . . . . . . . . . . 15 (((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ 𝑐𝑃) ∧ (𝑥𝑠𝑦𝑡)) → 𝑦𝐵)
16776ad4antr 731 . . . . . . . . . . . . . . . 16 (((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ 𝑐𝑃) ∧ (𝑥𝑠𝑦𝑡)) → 𝐹:𝑃𝐵)
168 simplr 768 . . . . . . . . . . . . . . . 16 (((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ 𝑐𝑃) ∧ (𝑥𝑠𝑦𝑡)) → 𝑐𝑃)
169167, 168ffvelcdmd 7090 . . . . . . . . . . . . . . 15 (((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ 𝑐𝑃) ∧ (𝑥𝑠𝑦𝑡)) → (𝐹𝑐) ∈ 𝐵)
1703, 4, 5, 17, 18, 19, 158, 160, 162, 164, 166, 169f1otrgitv 28668 . . . . . . . . . . . . . 14 (((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ 𝑐𝑃) ∧ (𝑥𝑠𝑦𝑡)) → ((𝐹𝑐) ∈ (𝑥𝐽𝑦) ↔ (𝐹‘(𝐹𝑐)) ∈ ((𝐹𝑥)𝐼(𝐹𝑦))))
171170adantlr 714 . . . . . . . . . . . . 13 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ 𝑐𝑃) ∧ ∀𝑒 ∈ (𝐹𝑠)∀𝑓 ∈ (𝐹𝑡)𝑐 ∈ (𝑒𝐼𝑓)) ∧ (𝑥𝑠𝑦𝑡)) → ((𝐹𝑐) ∈ (𝑥𝐽𝑦) ↔ (𝐹‘(𝐹𝑐)) ∈ ((𝐹𝑥)𝐼(𝐹𝑦))))
172157, 171mpbird 257 . . . . . . . . . . . 12 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ 𝑐𝑃) ∧ ∀𝑒 ∈ (𝐹𝑠)∀𝑓 ∈ (𝐹𝑡)𝑐 ∈ (𝑒𝐼𝑓)) ∧ (𝑥𝑠𝑦𝑡)) → (𝐹𝑐) ∈ (𝑥𝐽𝑦))
173172ralrimivva 3196 . . . . . . . . . . 11 (((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ 𝑐𝑃) ∧ ∀𝑒 ∈ (𝐹𝑠)∀𝑓 ∈ (𝐹𝑡)𝑐 ∈ (𝑒𝐼𝑓)) → ∀𝑥𝑠𝑦𝑡 (𝐹𝑐) ∈ (𝑥𝐽𝑦))
174173adantllr 718 . . . . . . . . . 10 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑐𝑃) ∧ ∀𝑒 ∈ (𝐹𝑠)∀𝑓 ∈ (𝐹𝑡)𝑐 ∈ (𝑒𝐼𝑓)) → ∀𝑥𝑠𝑦𝑡 (𝐹𝑐) ∈ (𝑥𝐽𝑦))
17576ad4antr 731 . . . . . . . . . . . . 13 (((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑐𝑃) → 𝐹:𝑃𝐵)
176 simpr 484 . . . . . . . . . . . . 13 (((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑐𝑃) → 𝑐𝑃)
177175, 176ffvelcdmd 7090 . . . . . . . . . . . 12 (((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑐𝑃) → (𝐹𝑐) ∈ 𝐵)
178 eleq1 2817 . . . . . . . . . . . . . 14 (𝑏 = (𝐹𝑐) → (𝑏 ∈ (𝑥𝐽𝑦) ↔ (𝐹𝑐) ∈ (𝑥𝐽𝑦)))
1791782ralbidv 3214 . . . . . . . . . . . . 13 (𝑏 = (𝐹𝑐) → (∀𝑥𝑠𝑦𝑡 𝑏 ∈ (𝑥𝐽𝑦) ↔ ∀𝑥𝑠𝑦𝑡 (𝐹𝑐) ∈ (𝑥𝐽𝑦)))
180179adantl 481 . . . . . . . . . . . 12 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑐𝑃) ∧ 𝑏 = (𝐹𝑐)) → (∀𝑥𝑠𝑦𝑡 𝑏 ∈ (𝑥𝐽𝑦) ↔ ∀𝑥𝑠𝑦𝑡 (𝐹𝑐) ∈ (𝑥𝐽𝑦)))
181177, 180rspcedv 3601 . . . . . . . . . . 11 (((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑐𝑃) → (∀𝑥𝑠𝑦𝑡 (𝐹𝑐) ∈ (𝑥𝐽𝑦) → ∃𝑏𝐵𝑥𝑠𝑦𝑡 𝑏 ∈ (𝑥𝐽𝑦)))
182181adantr 480 . . . . . . . . . 10 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑐𝑃) ∧ ∀𝑒 ∈ (𝐹𝑠)∀𝑓 ∈ (𝐹𝑡)𝑐 ∈ (𝑒𝐼𝑓)) → (∀𝑥𝑠𝑦𝑡 (𝐹𝑐) ∈ (𝑥𝐽𝑦) → ∃𝑏𝐵𝑥𝑠𝑦𝑡 𝑏 ∈ (𝑥𝐽𝑦)))
183174, 182mpd 15 . . . . . . . . 9 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑐𝑃) ∧ ∀𝑒 ∈ (𝐹𝑠)∀𝑓 ∈ (𝐹𝑡)𝑐 ∈ (𝑒𝐼𝑓)) → ∃𝑏𝐵𝑥𝑠𝑦𝑡 𝑏 ∈ (𝑥𝐽𝑦))
1846ad3antrrr 729 . . . . . . . . . 10 ((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) → 𝐺 ∈ TarskiG)
185 imassrn 6069 . . . . . . . . . . 11 (𝐹𝑠) ⊆ ran 𝐹
186 f1ofo 6841 . . . . . . . . . . . . 13 (𝐹:𝐵1-1-onto𝑃𝐹:𝐵onto𝑃)
187 forn 6809 . . . . . . . . . . . . 13 (𝐹:𝐵onto𝑃 → ran 𝐹 = 𝑃)
1888, 186, 1873syl 18 . . . . . . . . . . . 12 (𝜑 → ran 𝐹 = 𝑃)
189188ad3antrrr 729 . . . . . . . . . . 11 ((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) → ran 𝐹 = 𝑃)
190185, 189sseqtrid 4031 . . . . . . . . . 10 ((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) → (𝐹𝑠) ⊆ 𝑃)
191 imassrn 6069 . . . . . . . . . . 11 (𝐹𝑡) ⊆ ran 𝐹
192191, 189sseqtrid 4031 . . . . . . . . . 10 ((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) → (𝐹𝑡) ⊆ 𝑃)
19310ad3antrrr 729 . . . . . . . . . . 11 ((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) → 𝐹:𝐵𝑃)
194 simplr 768 . . . . . . . . . . 11 ((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) → 𝑎𝐵)
195193, 194ffvelcdmd 7090 . . . . . . . . . 10 ((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) → (𝐹𝑎) ∈ 𝑃)
1968ad5antr 733 . . . . . . . . . . . . . . . . 17 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹𝑠)) ∧ 𝑣 ∈ (𝐹𝑡)) → 𝐹:𝐵1-1-onto𝑃)
197 ffn 6717 . . . . . . . . . . . . . . . . 17 (𝐹:𝑃𝐵𝐹 Fn 𝑃)
198196, 74, 75, 1974syl 19 . . . . . . . . . . . . . . . 16 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹𝑠)) ∧ 𝑣 ∈ (𝐹𝑡)) → 𝐹 Fn 𝑃)
199190ad2antrr 725 . . . . . . . . . . . . . . . 16 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹𝑠)) ∧ 𝑣 ∈ (𝐹𝑡)) → (𝐹𝑠) ⊆ 𝑃)
200 simplr 768 . . . . . . . . . . . . . . . 16 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹𝑠)) ∧ 𝑣 ∈ (𝐹𝑡)) → 𝑢 ∈ (𝐹𝑠))
201 fnfvima 7240 . . . . . . . . . . . . . . . 16 ((𝐹 Fn 𝑃 ∧ (𝐹𝑠) ⊆ 𝑃𝑢 ∈ (𝐹𝑠)) → (𝐹𝑢) ∈ (𝐹 “ (𝐹𝑠)))
202198, 199, 200, 201syl3anc 1369 . . . . . . . . . . . . . . 15 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹𝑠)) ∧ 𝑣 ∈ (𝐹𝑡)) → (𝐹𝑢) ∈ (𝐹 “ (𝐹𝑠)))
203196, 29syl 17 . . . . . . . . . . . . . . . 16 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹𝑠)) ∧ 𝑣 ∈ (𝐹𝑡)) → 𝐹:𝐵1-1𝑃)
204 simp-5r 785 . . . . . . . . . . . . . . . . . 18 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹𝑠)) ∧ 𝑣 ∈ (𝐹𝑡)) → (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵))
205204simpld 494 . . . . . . . . . . . . . . . . 17 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹𝑠)) ∧ 𝑣 ∈ (𝐹𝑡)) → 𝑠 ∈ 𝒫 𝐵)
206205elpwid 4608 . . . . . . . . . . . . . . . 16 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹𝑠)) ∧ 𝑣 ∈ (𝐹𝑡)) → 𝑠𝐵)
207 f1imacnv 6850 . . . . . . . . . . . . . . . 16 ((𝐹:𝐵1-1𝑃𝑠𝐵) → (𝐹 “ (𝐹𝑠)) = 𝑠)
208203, 206, 207syl2anc 583 . . . . . . . . . . . . . . 15 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹𝑠)) ∧ 𝑣 ∈ (𝐹𝑡)) → (𝐹 “ (𝐹𝑠)) = 𝑠)
209202, 208eleqtrd 2831 . . . . . . . . . . . . . 14 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹𝑠)) ∧ 𝑣 ∈ (𝐹𝑡)) → (𝐹𝑢) ∈ 𝑠)
210192ad2antrr 725 . . . . . . . . . . . . . . . 16 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹𝑠)) ∧ 𝑣 ∈ (𝐹𝑡)) → (𝐹𝑡) ⊆ 𝑃)
211 simpr 484 . . . . . . . . . . . . . . . 16 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹𝑠)) ∧ 𝑣 ∈ (𝐹𝑡)) → 𝑣 ∈ (𝐹𝑡))
212 fnfvima 7240 . . . . . . . . . . . . . . . 16 ((𝐹 Fn 𝑃 ∧ (𝐹𝑡) ⊆ 𝑃𝑣 ∈ (𝐹𝑡)) → (𝐹𝑣) ∈ (𝐹 “ (𝐹𝑡)))
213198, 210, 211, 212syl3anc 1369 . . . . . . . . . . . . . . 15 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹𝑠)) ∧ 𝑣 ∈ (𝐹𝑡)) → (𝐹𝑣) ∈ (𝐹 “ (𝐹𝑡)))
214204simprd 495 . . . . . . . . . . . . . . . . 17 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹𝑠)) ∧ 𝑣 ∈ (𝐹𝑡)) → 𝑡 ∈ 𝒫 𝐵)
215214elpwid 4608 . . . . . . . . . . . . . . . 16 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹𝑠)) ∧ 𝑣 ∈ (𝐹𝑡)) → 𝑡𝐵)
216 f1imacnv 6850 . . . . . . . . . . . . . . . 16 ((𝐹:𝐵1-1𝑃𝑡𝐵) → (𝐹 “ (𝐹𝑡)) = 𝑡)
217203, 215, 216syl2anc 583 . . . . . . . . . . . . . . 15 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹𝑠)) ∧ 𝑣 ∈ (𝐹𝑡)) → (𝐹 “ (𝐹𝑡)) = 𝑡)
218213, 217eleqtrd 2831 . . . . . . . . . . . . . 14 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹𝑠)) ∧ 𝑣 ∈ (𝐹𝑡)) → (𝐹𝑣) ∈ 𝑡)
219 simpllr 775 . . . . . . . . . . . . . 14 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹𝑠)) ∧ 𝑣 ∈ (𝐹𝑡)) → ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦))
220 eleq1 2817 . . . . . . . . . . . . . . 15 (𝑥 = (𝐹𝑢) → (𝑥 ∈ (𝑎𝐽𝑦) ↔ (𝐹𝑢) ∈ (𝑎𝐽𝑦)))
221 oveq2 7423 . . . . . . . . . . . . . . . 16 (𝑦 = (𝐹𝑣) → (𝑎𝐽𝑦) = (𝑎𝐽(𝐹𝑣)))
222221eleq2d 2815 . . . . . . . . . . . . . . 15 (𝑦 = (𝐹𝑣) → ((𝐹𝑢) ∈ (𝑎𝐽𝑦) ↔ (𝐹𝑢) ∈ (𝑎𝐽(𝐹𝑣))))
223220, 222rspc2va 3620 . . . . . . . . . . . . . 14 ((((𝐹𝑢) ∈ 𝑠 ∧ (𝐹𝑣) ∈ 𝑡) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) → (𝐹𝑢) ∈ (𝑎𝐽(𝐹𝑣)))
224209, 218, 219, 223syl21anc 837 . . . . . . . . . . . . 13 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹𝑠)) ∧ 𝑣 ∈ (𝐹𝑡)) → (𝐹𝑢) ∈ (𝑎𝐽(𝐹𝑣)))
225 simp-6l 786 . . . . . . . . . . . . . . 15 (((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹𝑠)) ∧ 𝑣 ∈ (𝐹𝑡)) ∧ (𝑒𝐵𝑓𝐵)) → 𝜑)
226225, 21sylancom 587 . . . . . . . . . . . . . 14 (((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹𝑠)) ∧ 𝑣 ∈ (𝐹𝑡)) ∧ (𝑒𝐵𝑓𝐵)) → (𝑒𝐸𝑓) = ((𝐹𝑒)𝐷(𝐹𝑓)))
227 simp-6l 786 . . . . . . . . . . . . . . 15 (((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹𝑠)) ∧ 𝑣 ∈ (𝐹𝑡)) ∧ (𝑒𝐵𝑓𝐵𝑔𝐵)) → 𝜑)
228227, 23sylancom 587 . . . . . . . . . . . . . 14 (((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹𝑠)) ∧ 𝑣 ∈ (𝐹𝑡)) ∧ (𝑒𝐵𝑓𝐵𝑔𝐵)) → (𝑔 ∈ (𝑒𝐽𝑓) ↔ (𝐹𝑔) ∈ ((𝐹𝑒)𝐼(𝐹𝑓))))
229 simp-4r 783 . . . . . . . . . . . . . 14 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹𝑠)) ∧ 𝑣 ∈ (𝐹𝑡)) → 𝑎𝐵)
230210, 211sseldd 3980 . . . . . . . . . . . . . . 15 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹𝑠)) ∧ 𝑣 ∈ (𝐹𝑡)) → 𝑣𝑃)
231 f1ocnvdm 7289 . . . . . . . . . . . . . . 15 ((𝐹:𝐵1-1-onto𝑃𝑣𝑃) → (𝐹𝑣) ∈ 𝐵)
232196, 230, 231syl2anc 583 . . . . . . . . . . . . . 14 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹𝑠)) ∧ 𝑣 ∈ (𝐹𝑡)) → (𝐹𝑣) ∈ 𝐵)
233199, 200sseldd 3980 . . . . . . . . . . . . . . 15 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹𝑠)) ∧ 𝑣 ∈ (𝐹𝑡)) → 𝑢𝑃)
234 f1ocnvdm 7289 . . . . . . . . . . . . . . 15 ((𝐹:𝐵1-1-onto𝑃𝑢𝑃) → (𝐹𝑢) ∈ 𝐵)
235196, 233, 234syl2anc 583 . . . . . . . . . . . . . 14 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹𝑠)) ∧ 𝑣 ∈ (𝐹𝑡)) → (𝐹𝑢) ∈ 𝐵)
2363, 4, 5, 17, 18, 19, 196, 226, 228, 229, 232, 235f1otrgitv 28668 . . . . . . . . . . . . 13 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹𝑠)) ∧ 𝑣 ∈ (𝐹𝑡)) → ((𝐹𝑢) ∈ (𝑎𝐽(𝐹𝑣)) ↔ (𝐹‘(𝐹𝑢)) ∈ ((𝐹𝑎)𝐼(𝐹‘(𝐹𝑣)))))
237224, 236mpbid 231 . . . . . . . . . . . 12 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹𝑠)) ∧ 𝑣 ∈ (𝐹𝑡)) → (𝐹‘(𝐹𝑢)) ∈ ((𝐹𝑎)𝐼(𝐹‘(𝐹𝑣))))
238 f1ocnvfv2 7281 . . . . . . . . . . . . 13 ((𝐹:𝐵1-1-onto𝑃𝑢𝑃) → (𝐹‘(𝐹𝑢)) = 𝑢)
239196, 233, 238syl2anc 583 . . . . . . . . . . . 12 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹𝑠)) ∧ 𝑣 ∈ (𝐹𝑡)) → (𝐹‘(𝐹𝑢)) = 𝑢)
240 f1ocnvfv2 7281 . . . . . . . . . . . . . 14 ((𝐹:𝐵1-1-onto𝑃𝑣𝑃) → (𝐹‘(𝐹𝑣)) = 𝑣)
241196, 230, 240syl2anc 583 . . . . . . . . . . . . 13 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹𝑠)) ∧ 𝑣 ∈ (𝐹𝑡)) → (𝐹‘(𝐹𝑣)) = 𝑣)
242241oveq2d 7431 . . . . . . . . . . . 12 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹𝑠)) ∧ 𝑣 ∈ (𝐹𝑡)) → ((𝐹𝑎)𝐼(𝐹‘(𝐹𝑣))) = ((𝐹𝑎)𝐼𝑣))
243237, 239, 2423eltr3d 2843 . . . . . . . . . . 11 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹𝑠)) ∧ 𝑣 ∈ (𝐹𝑡)) → 𝑢 ∈ ((𝐹𝑎)𝐼𝑣))
2442433impa 1108 . . . . . . . . . 10 (((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹𝑠) ∧ 𝑣 ∈ (𝐹𝑡)) → 𝑢 ∈ ((𝐹𝑎)𝐼𝑣))
2453, 4, 5, 184, 190, 192, 195, 244axtgcont 28267 . . . . . . . . 9 ((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) → ∃𝑐𝑃𝑒 ∈ (𝐹𝑠)∀𝑓 ∈ (𝐹𝑡)𝑐 ∈ (𝑒𝐼𝑓))
246183, 245r19.29a 3158 . . . . . . . 8 ((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) → ∃𝑏𝐵𝑥𝑠𝑦𝑡 𝑏 ∈ (𝑥𝐽𝑦))
247246rexlimdva2 3153 . . . . . . 7 ((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) → (∃𝑎𝐵𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦) → ∃𝑏𝐵𝑥𝑠𝑦𝑡 𝑏 ∈ (𝑥𝐽𝑦)))
248247ralrimivva 3196 . . . . . 6 (𝜑 → ∀𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵(∃𝑎𝐵𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦) → ∃𝑏𝐵𝑥𝑠𝑦𝑡 𝑏 ∈ (𝑥𝐽𝑦)))
24973, 131, 2483jca 1126 . . . . 5 (𝜑 → (∀𝑥𝐵𝑦𝐵 (𝑦 ∈ (𝑥𝐽𝑥) → 𝑥 = 𝑦) ∧ ∀𝑥𝐵𝑦𝐵𝑧𝐵𝑢𝐵𝑣𝐵 ((𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧)) → ∃𝑎𝐵 (𝑎 ∈ (𝑢𝐽𝑦) ∧ 𝑎 ∈ (𝑣𝐽𝑥))) ∧ ∀𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵(∃𝑎𝐵𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦) → ∃𝑏𝐵𝑥𝑠𝑦𝑡 𝑏 ∈ (𝑥𝐽𝑦))))
25017, 18, 19istrkgb 28253 . . . . 5 (𝐻 ∈ TarskiGB ↔ (𝐻 ∈ V ∧ (∀𝑥𝐵𝑦𝐵 (𝑦 ∈ (𝑥𝐽𝑥) → 𝑥 = 𝑦) ∧ ∀𝑥𝐵𝑦𝐵𝑧𝐵𝑢𝐵𝑣𝐵 ((𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧)) → ∃𝑎𝐵 (𝑎 ∈ (𝑢𝐽𝑦) ∧ 𝑎 ∈ (𝑣𝐽𝑥))) ∧ ∀𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵(∃𝑎𝐵𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦) → ∃𝑏𝐵𝑥𝑠𝑦𝑡 𝑏 ∈ (𝑥𝐽𝑦)))))
2512, 249, 250sylanbrc 582 . . . 4 (𝜑𝐻 ∈ TarskiGB)
25256, 251elind 4191 . . 3 (𝜑𝐻 ∈ (TarskiGC ∩ TarskiGB))
2536ad9antr 741 . . . . . . . . . . . . . . . . 17 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → 𝐺 ∈ TarskiG)
25410ad9antr 741 . . . . . . . . . . . . . . . . . 18 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → 𝐹:𝐵𝑃)
255 simp-9r 793 . . . . . . . . . . . . . . . . . 18 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → 𝑥𝐵)
256254, 255ffvelcdmd 7090 . . . . . . . . . . . . . . . . 17 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → (𝐹𝑥) ∈ 𝑃)
257 simp-8r 791 . . . . . . . . . . . . . . . . . 18 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → 𝑦𝐵)
258254, 257ffvelcdmd 7090 . . . . . . . . . . . . . . . . 17 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → (𝐹𝑦) ∈ 𝑃)
259 simp-7r 789 . . . . . . . . . . . . . . . . . 18 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → 𝑧𝐵)
260254, 259ffvelcdmd 7090 . . . . . . . . . . . . . . . . 17 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → (𝐹𝑧) ∈ 𝑃)
261 simp-5r 785 . . . . . . . . . . . . . . . . . 18 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → 𝑎𝐵)
262254, 261ffvelcdmd 7090 . . . . . . . . . . . . . . . . 17 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → (𝐹𝑎) ∈ 𝑃)
263 simp-4r 783 . . . . . . . . . . . . . . . . . 18 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → 𝑏𝐵)
264254, 263ffvelcdmd 7090 . . . . . . . . . . . . . . . . 17 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → (𝐹𝑏) ∈ 𝑃)
265 simpllr 775 . . . . . . . . . . . . . . . . . 18 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → 𝑐𝐵)
266254, 265ffvelcdmd 7090 . . . . . . . . . . . . . . . . 17 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → (𝐹𝑐) ∈ 𝑃)
267 simp-6r 787 . . . . . . . . . . . . . . . . . 18 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → 𝑢𝐵)
268254, 267ffvelcdmd 7090 . . . . . . . . . . . . . . . . 17 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → (𝐹𝑢) ∈ 𝑃)
269 simplr 768 . . . . . . . . . . . . . . . . . 18 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → 𝑣𝐵)
270254, 269ffvelcdmd 7090 . . . . . . . . . . . . . . . . 17 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → (𝐹𝑣) ∈ 𝑃)
2718ad9antr 741 . . . . . . . . . . . . . . . . . . 19 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → 𝐹:𝐵1-1-onto𝑃)
272271, 255jca 511 . . . . . . . . . . . . . . . . . 18 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → (𝐹:𝐵1-1-onto𝑃𝑥𝐵))
273 simprl1 1216 . . . . . . . . . . . . . . . . . 18 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → 𝑥𝑦)
274 dff1o6 7279 . . . . . . . . . . . . . . . . . . . . . . 23 (𝐹:𝐵1-1-onto𝑃 ↔ (𝐹 Fn 𝐵 ∧ ran 𝐹 = 𝑃 ∧ ∀𝑥𝐵𝑦𝐵 ((𝐹𝑥) = (𝐹𝑦) → 𝑥 = 𝑦)))
275274simp3bi 1145 . . . . . . . . . . . . . . . . . . . . . 22 (𝐹:𝐵1-1-onto𝑃 → ∀𝑥𝐵𝑦𝐵 ((𝐹𝑥) = (𝐹𝑦) → 𝑥 = 𝑦))
276275r19.21bi 3244 . . . . . . . . . . . . . . . . . . . . 21 ((𝐹:𝐵1-1-onto𝑃𝑥𝐵) → ∀𝑦𝐵 ((𝐹𝑥) = (𝐹𝑦) → 𝑥 = 𝑦))
277276r19.21bi 3244 . . . . . . . . . . . . . . . . . . . 20 (((𝐹:𝐵1-1-onto𝑃𝑥𝐵) ∧ 𝑦𝐵) → ((𝐹𝑥) = (𝐹𝑦) → 𝑥 = 𝑦))
278277necon3d 2957 . . . . . . . . . . . . . . . . . . 19 (((𝐹:𝐵1-1-onto𝑃𝑥𝐵) ∧ 𝑦𝐵) → (𝑥𝑦 → (𝐹𝑥) ≠ (𝐹𝑦)))
279278imp 406 . . . . . . . . . . . . . . . . . 18 ((((𝐹:𝐵1-1-onto𝑃𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑥𝑦) → (𝐹𝑥) ≠ (𝐹𝑦))
280272, 257, 273, 279syl21anc 837 . . . . . . . . . . . . . . . . 17 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → (𝐹𝑥) ≠ (𝐹𝑦))
281 simprl2 1217 . . . . . . . . . . . . . . . . . 18 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → 𝑦 ∈ (𝑥𝐽𝑧))
28221ex 412 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → ((𝑒𝐵𝑓𝐵) → (𝑒𝐸𝑓) = ((𝐹𝑒)𝐷(𝐹𝑓))))
283282ad9antr 741 . . . . . . . . . . . . . . . . . . . 20 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → ((𝑒𝐵𝑓𝐵) → (𝑒𝐸𝑓) = ((𝐹𝑒)𝐷(𝐹𝑓))))
284283imp 406 . . . . . . . . . . . . . . . . . . 19 (((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) ∧ (𝑒𝐵𝑓𝐵)) → (𝑒𝐸𝑓) = ((𝐹𝑒)𝐷(𝐹𝑓)))
28523ex 412 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → ((𝑒𝐵𝑓𝐵𝑔𝐵) → (𝑔 ∈ (𝑒𝐽𝑓) ↔ (𝐹𝑔) ∈ ((𝐹𝑒)𝐼(𝐹𝑓)))))
286285ad9antr 741 . . . . . . . . . . . . . . . . . . . 20 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → ((𝑒𝐵𝑓𝐵𝑔𝐵) → (𝑔 ∈ (𝑒𝐽𝑓) ↔ (𝐹𝑔) ∈ ((𝐹𝑒)𝐼(𝐹𝑓)))))
287286imp 406 . . . . . . . . . . . . . . . . . . 19 (((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) ∧ (𝑒𝐵𝑓𝐵𝑔𝐵)) → (𝑔 ∈ (𝑒𝐽𝑓) ↔ (𝐹𝑔) ∈ ((𝐹𝑒)𝐼(𝐹𝑓))))
2883, 4, 5, 17, 18, 19, 271, 284, 287, 255, 259, 257f1otrgitv 28668 . . . . . . . . . . . . . . . . . 18 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → (𝑦 ∈ (𝑥𝐽𝑧) ↔ (𝐹𝑦) ∈ ((𝐹𝑥)𝐼(𝐹𝑧))))
289281, 288mpbid 231 . . . . . . . . . . . . . . . . 17 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → (𝐹𝑦) ∈ ((𝐹𝑥)𝐼(𝐹𝑧)))
290 simprl3 1218 . . . . . . . . . . . . . . . . . 18 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → 𝑏 ∈ (𝑎𝐽𝑐))
2913, 4, 5, 17, 18, 19, 271, 284, 287, 261, 265, 263f1otrgitv 28668 . . . . . . . . . . . . . . . . . 18 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → (𝑏 ∈ (𝑎𝐽𝑐) ↔ (𝐹𝑏) ∈ ((𝐹𝑎)𝐼(𝐹𝑐))))
292290, 291mpbid 231 . . . . . . . . . . . . . . . . 17 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → (𝐹𝑏) ∈ ((𝐹𝑎)𝐼(𝐹𝑐)))
293 simprr 772 . . . . . . . . . . . . . . . . . . . 20 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))
294293simpld 494 . . . . . . . . . . . . . . . . . . 19 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → ((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)))
295294simpld 494 . . . . . . . . . . . . . . . . . 18 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → (𝑥𝐸𝑦) = (𝑎𝐸𝑏))
2963, 4, 5, 17, 18, 19, 271, 284, 287, 255, 257f1otrgds 28667 . . . . . . . . . . . . . . . . . 18 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → (𝑥𝐸𝑦) = ((𝐹𝑥)𝐷(𝐹𝑦)))
2973, 4, 5, 17, 18, 19, 271, 284, 287, 261, 263f1otrgds 28667 . . . . . . . . . . . . . . . . . 18 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → (𝑎𝐸𝑏) = ((𝐹𝑎)𝐷(𝐹𝑏)))
298295, 296, 2973eqtr3d 2776 . . . . . . . . . . . . . . . . 17 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → ((𝐹𝑥)𝐷(𝐹𝑦)) = ((𝐹𝑎)𝐷(𝐹𝑏)))
299294simprd 495 . . . . . . . . . . . . . . . . . 18 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → (𝑦𝐸𝑧) = (𝑏𝐸𝑐))
3003, 4, 5, 17, 18, 19, 271, 284, 287, 257, 259f1otrgds 28667 . . . . . . . . . . . . . . . . . 18 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → (𝑦𝐸𝑧) = ((𝐹𝑦)𝐷(𝐹𝑧)))
3013, 4, 5, 17, 18, 19, 271, 284, 287, 263, 265f1otrgds 28667 . . . . . . . . . . . . . . . . . 18 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → (𝑏𝐸𝑐) = ((𝐹𝑏)𝐷(𝐹𝑐)))
302299, 300, 3013eqtr3d 2776 . . . . . . . . . . . . . . . . 17 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → ((𝐹𝑦)𝐷(𝐹𝑧)) = ((𝐹𝑏)𝐷(𝐹𝑐)))
303293simprd 495 . . . . . . . . . . . . . . . . . . 19 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣)))
304303simpld 494 . . . . . . . . . . . . . . . . . 18 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → (𝑥𝐸𝑢) = (𝑎𝐸𝑣))
3053, 4, 5, 17, 18, 19, 271, 284, 287, 255, 267f1otrgds 28667 . . . . . . . . . . . . . . . . . 18 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → (𝑥𝐸𝑢) = ((𝐹𝑥)𝐷(𝐹𝑢)))
3063, 4, 5, 17, 18, 19, 271, 284, 287, 261, 269f1otrgds 28667 . . . . . . . . . . . . . . . . . 18 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → (𝑎𝐸𝑣) = ((𝐹𝑎)𝐷(𝐹𝑣)))
307304, 305, 3063eqtr3d 2776 . . . . . . . . . . . . . . . . 17 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → ((𝐹𝑥)𝐷(𝐹𝑢)) = ((𝐹𝑎)𝐷(𝐹𝑣)))
308303simprd 495 . . . . . . . . . . . . . . . . . 18 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → (𝑦𝐸𝑢) = (𝑏𝐸𝑣))
3093, 4, 5, 17, 18, 19, 271, 284, 287, 257, 267f1otrgds 28667 . . . . . . . . . . . . . . . . . 18 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → (𝑦𝐸𝑢) = ((𝐹𝑦)𝐷(𝐹𝑢)))
3103, 4, 5, 17, 18, 19, 271, 284, 287, 263, 269f1otrgds 28667 . . . . . . . . . . . . . . . . . 18 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → (𝑏𝐸𝑣) = ((𝐹𝑏)𝐷(𝐹𝑣)))
311308, 309, 3103eqtr3d 2776 . . . . . . . . . . . . . . . . 17 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → ((𝐹𝑦)𝐷(𝐹𝑢)) = ((𝐹𝑏)𝐷(𝐹𝑣)))
3123, 4, 5, 253, 256, 258, 260, 262, 264, 266, 268, 270, 280, 289, 292, 298, 302, 307, 311axtg5seg 28263 . . . . . . . . . . . . . . . 16 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → ((𝐹𝑧)𝐷(𝐹𝑢)) = ((𝐹𝑐)𝐷(𝐹𝑣)))
3133, 4, 5, 17, 18, 19, 271, 284, 287, 259, 267f1otrgds 28667 . . . . . . . . . . . . . . . 16 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → (𝑧𝐸𝑢) = ((𝐹𝑧)𝐷(𝐹𝑢)))
3143, 4, 5, 17, 18, 19, 271, 284, 287, 265, 269f1otrgds 28667 . . . . . . . . . . . . . . . 16 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → (𝑐𝐸𝑣) = ((𝐹𝑐)𝐷(𝐹𝑣)))
315312, 313, 3143eqtr4d 2778 . . . . . . . . . . . . . . 15 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → (𝑧𝐸𝑢) = (𝑐𝐸𝑣))
316315ex 412 . . . . . . . . . . . . . 14 (((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) → (((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣)))) → (𝑧𝐸𝑢) = (𝑐𝐸𝑣)))
317316ralrimiva 3142 . . . . . . . . . . . . 13 ((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) → ∀𝑣𝐵 (((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣)))) → (𝑧𝐸𝑢) = (𝑐𝐸𝑣)))
318317ralrimiva 3142 . . . . . . . . . . . 12 (((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) → ∀𝑐𝐵𝑣𝐵 (((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣)))) → (𝑧𝐸𝑢) = (𝑐𝐸𝑣)))
319318ralrimiva 3142 . . . . . . . . . . 11 ((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) → ∀𝑏𝐵𝑐𝐵𝑣𝐵 (((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣)))) → (𝑧𝐸𝑢) = (𝑐𝐸𝑣)))
320319ralrimiva 3142 . . . . . . . . . 10 (((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) → ∀𝑎𝐵𝑏𝐵𝑐𝐵𝑣𝐵 (((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣)))) → (𝑧𝐸𝑢) = (𝑐𝐸𝑣)))
321320ralrimiva 3142 . . . . . . . . 9 ((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) → ∀𝑢𝐵𝑎𝐵𝑏𝐵𝑐𝐵𝑣𝐵 (((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣)))) → (𝑧𝐸𝑢) = (𝑐𝐸𝑣)))
322321ralrimiva 3142 . . . . . . . 8 (((𝜑𝑥𝐵) ∧ 𝑦𝐵) → ∀𝑧𝐵𝑢𝐵𝑎𝐵𝑏𝐵𝑐𝐵𝑣𝐵 (((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣)))) → (𝑧𝐸𝑢) = (𝑐𝐸𝑣)))
323322ralrimiva 3142 . . . . . . 7 ((𝜑𝑥𝐵) → ∀𝑦𝐵𝑧𝐵𝑢𝐵𝑎𝐵𝑏𝐵𝑐𝐵𝑣𝐵 (((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣)))) → (𝑧𝐸𝑢) = (𝑐𝐸𝑣)))
324323ralrimiva 3142 . . . . . 6 (𝜑 → ∀𝑥𝐵𝑦𝐵𝑧𝐵𝑢𝐵𝑎𝐵𝑏𝐵𝑐𝐵𝑣𝐵 (((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣)))) → (𝑧𝐸𝑢) = (𝑐𝐸𝑣)))
325 simp-4l 782 . . . . . . . . . 10 (((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑎𝐵𝑏𝐵)) ∧ 𝑤𝑃) ∧ ((𝐹𝑦) ∈ ((𝐹𝑥)𝐼𝑤) ∧ ((𝐹𝑦)𝐷𝑤) = ((𝐹𝑎)𝐷(𝐹𝑏)))) → 𝜑)
326 simplr 768 . . . . . . . . . 10 (((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑎𝐵𝑏𝐵)) ∧ 𝑤𝑃) ∧ ((𝐹𝑦) ∈ ((𝐹𝑥)𝐼𝑤) ∧ ((𝐹𝑦)𝐷𝑤) = ((𝐹𝑎)𝐷(𝐹𝑏)))) → 𝑤𝑃)
327 simprl 770 . . . . . . . . . . . 12 (((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑎𝐵𝑏𝐵)) ∧ 𝑤𝑃) ∧ ((𝐹𝑦) ∈ ((𝐹𝑥)𝐼𝑤) ∧ ((𝐹𝑦)𝐷𝑤) = ((𝐹𝑎)𝐷(𝐹𝑏)))) → (𝐹𝑦) ∈ ((𝐹𝑥)𝐼𝑤))
328325, 8syl 17 . . . . . . . . . . . . . 14 (((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑎𝐵𝑏𝐵)) ∧ 𝑤𝑃) ∧ ((𝐹𝑦) ∈ ((𝐹𝑥)𝐼𝑤) ∧ ((𝐹𝑦)𝐷𝑤) = ((𝐹𝑎)𝐷(𝐹𝑏)))) → 𝐹:𝐵1-1-onto𝑃)
329 f1ocnvfv2 7281 . . . . . . . . . . . . . 14 ((𝐹:𝐵1-1-onto𝑃𝑤𝑃) → (𝐹‘(𝐹𝑤)) = 𝑤)
330328, 326, 329syl2anc 583 . . . . . . . . . . . . 13 (((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑎𝐵𝑏𝐵)) ∧ 𝑤𝑃) ∧ ((𝐹𝑦) ∈ ((𝐹𝑥)𝐼𝑤) ∧ ((𝐹𝑦)𝐷𝑤) = ((𝐹𝑎)𝐷(𝐹𝑏)))) → (𝐹‘(𝐹𝑤)) = 𝑤)
331330oveq2d 7431 . . . . . . . . . . . 12 (((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑎𝐵𝑏𝐵)) ∧ 𝑤𝑃) ∧ ((𝐹𝑦) ∈ ((𝐹𝑥)𝐼𝑤) ∧ ((𝐹𝑦)𝐷𝑤) = ((𝐹𝑎)𝐷(𝐹𝑏)))) → ((𝐹𝑥)𝐼(𝐹‘(𝐹𝑤))) = ((𝐹𝑥)𝐼𝑤))
332327, 331eleqtrrd 2832 . . . . . . . . . . 11 (((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑎𝐵𝑏𝐵)) ∧ 𝑤𝑃) ∧ ((𝐹𝑦) ∈ ((𝐹𝑥)𝐼𝑤) ∧ ((𝐹𝑦)𝐷𝑤) = ((𝐹𝑎)𝐷(𝐹𝑏)))) → (𝐹𝑦) ∈ ((𝐹𝑥)𝐼(𝐹‘(𝐹𝑤))))
333325, 21sylan 579 . . . . . . . . . . . 12 ((((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑎𝐵𝑏𝐵)) ∧ 𝑤𝑃) ∧ ((𝐹𝑦) ∈ ((𝐹𝑥)𝐼𝑤) ∧ ((𝐹𝑦)𝐷𝑤) = ((𝐹𝑎)𝐷(𝐹𝑏)))) ∧ (𝑒𝐵𝑓𝐵)) → (𝑒𝐸𝑓) = ((𝐹𝑒)𝐷(𝐹𝑓)))
334325, 23sylan 579 . . . . . . . . . . . 12 ((((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑎𝐵𝑏𝐵)) ∧ 𝑤𝑃) ∧ ((𝐹𝑦) ∈ ((𝐹𝑥)𝐼𝑤) ∧ ((𝐹𝑦)𝐷𝑤) = ((𝐹𝑎)𝐷(𝐹𝑏)))) ∧ (𝑒𝐵𝑓𝐵𝑔𝐵)) → (𝑔 ∈ (𝑒𝐽𝑓) ↔ (𝐹𝑔) ∈ ((𝐹𝑒)𝐼(𝐹𝑓))))
33512ad3antrrr 729 . . . . . . . . . . . 12 (((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑎𝐵𝑏𝐵)) ∧ 𝑤𝑃) ∧ ((𝐹𝑦) ∈ ((𝐹𝑥)𝐼𝑤) ∧ ((𝐹𝑦)𝐷𝑤) = ((𝐹𝑎)𝐷(𝐹𝑏)))) → 𝑥𝐵)
33676ffvelcdmda 7089 . . . . . . . . . . . . 13 ((𝜑𝑤𝑃) → (𝐹𝑤) ∈ 𝐵)
337325, 326, 336syl2anc 583 . . . . . . . . . . . 12 (((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑎𝐵𝑏𝐵)) ∧ 𝑤𝑃) ∧ ((𝐹𝑦) ∈ ((𝐹𝑥)𝐼𝑤) ∧ ((𝐹𝑦)𝐷𝑤) = ((𝐹𝑎)𝐷(𝐹𝑏)))) → (𝐹𝑤) ∈ 𝐵)
33814ad3antrrr 729 . . . . . . . . . . . 12 (((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑎𝐵𝑏𝐵)) ∧ 𝑤𝑃) ∧ ((𝐹𝑦) ∈ ((𝐹𝑥)𝐼𝑤) ∧ ((𝐹𝑦)𝐷𝑤) = ((𝐹𝑎)𝐷(𝐹𝑏)))) → 𝑦𝐵)
3393, 4, 5, 17, 18, 19, 328, 333, 334, 335, 337, 338f1otrgitv 28668 . . . . . . . . . . 11 (((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑎𝐵𝑏𝐵)) ∧ 𝑤𝑃) ∧ ((𝐹𝑦) ∈ ((𝐹𝑥)𝐼𝑤) ∧ ((𝐹𝑦)𝐷𝑤) = ((𝐹𝑎)𝐷(𝐹𝑏)))) → (𝑦 ∈ (𝑥𝐽(𝐹𝑤)) ↔ (𝐹𝑦) ∈ ((𝐹𝑥)𝐼(𝐹‘(𝐹𝑤)))))
340332, 339mpbird 257 . . . . . . . . . 10 (((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑎𝐵𝑏𝐵)) ∧ 𝑤𝑃) ∧ ((𝐹𝑦) ∈ ((𝐹𝑥)𝐼𝑤) ∧ ((𝐹𝑦)𝐷𝑤) = ((𝐹𝑎)𝐷(𝐹𝑏)))) → 𝑦 ∈ (𝑥𝐽(𝐹𝑤)))
3413, 4, 5, 17, 18, 19, 328, 333, 334, 338, 337f1otrgds 28667 . . . . . . . . . . . 12 (((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑎𝐵𝑏𝐵)) ∧ 𝑤𝑃) ∧ ((𝐹𝑦) ∈ ((𝐹𝑥)𝐼𝑤) ∧ ((𝐹𝑦)𝐷𝑤) = ((𝐹𝑎)𝐷(𝐹𝑏)))) → (𝑦𝐸(𝐹𝑤)) = ((𝐹𝑦)𝐷(𝐹‘(𝐹𝑤))))
342330oveq2d 7431 . . . . . . . . . . . 12 (((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑎𝐵𝑏𝐵)) ∧ 𝑤𝑃) ∧ ((𝐹𝑦) ∈ ((𝐹𝑥)𝐼𝑤) ∧ ((𝐹𝑦)𝐷𝑤) = ((𝐹𝑎)𝐷(𝐹𝑏)))) → ((𝐹𝑦)𝐷(𝐹‘(𝐹𝑤))) = ((𝐹𝑦)𝐷𝑤))
343 simprr 772 . . . . . . . . . . . 12 (((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑎𝐵𝑏𝐵)) ∧ 𝑤𝑃) ∧ ((𝐹𝑦) ∈ ((𝐹𝑥)𝐼𝑤) ∧ ((𝐹𝑦)𝐷𝑤) = ((𝐹𝑎)𝐷(𝐹𝑏)))) → ((𝐹𝑦)𝐷𝑤) = ((𝐹𝑎)𝐷(𝐹𝑏)))
344341, 342, 3433eqtrd 2772 . . . . . . . . . . 11 (((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑎𝐵𝑏𝐵)) ∧ 𝑤𝑃) ∧ ((𝐹𝑦) ∈ ((𝐹𝑥)𝐼𝑤) ∧ ((𝐹𝑦)𝐷𝑤) = ((𝐹𝑎)𝐷(𝐹𝑏)))) → (𝑦𝐸(𝐹𝑤)) = ((𝐹𝑎)𝐷(𝐹𝑏)))
345 simprl 770 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑎𝐵𝑏𝐵)) → 𝑎𝐵)
346345ad2antrr 725 . . . . . . . . . . . 12 (((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑎𝐵𝑏𝐵)) ∧ 𝑤𝑃) ∧ ((𝐹𝑦) ∈ ((𝐹𝑥)𝐼𝑤) ∧ ((𝐹𝑦)𝐷𝑤) = ((𝐹𝑎)𝐷(𝐹𝑏)))) → 𝑎𝐵)
347 simprr 772 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑎𝐵𝑏𝐵)) → 𝑏𝐵)
348347ad2antrr 725 . . . . . . . . . . . 12 (((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑎𝐵𝑏𝐵)) ∧ 𝑤𝑃) ∧ ((𝐹𝑦) ∈ ((𝐹𝑥)𝐼𝑤) ∧ ((𝐹𝑦)𝐷𝑤) = ((𝐹𝑎)𝐷(𝐹𝑏)))) → 𝑏𝐵)
3493, 4, 5, 17, 18, 19, 328, 333, 334, 346, 348f1otrgds 28667 . . . . . . . . . . 11 (((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑎𝐵𝑏𝐵)) ∧ 𝑤𝑃) ∧ ((𝐹𝑦) ∈ ((𝐹𝑥)𝐼𝑤) ∧ ((𝐹𝑦)𝐷𝑤) = ((𝐹𝑎)𝐷(𝐹𝑏)))) → (𝑎𝐸𝑏) = ((𝐹𝑎)𝐷(𝐹𝑏)))
350344, 349eqtr4d 2771 . . . . . . . . . 10 (((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑎𝐵𝑏𝐵)) ∧ 𝑤𝑃) ∧ ((𝐹𝑦) ∈ ((𝐹𝑥)𝐼𝑤) ∧ ((𝐹𝑦)𝐷𝑤) = ((𝐹𝑎)𝐷(𝐹𝑏)))) → (𝑦𝐸(𝐹𝑤)) = (𝑎𝐸𝑏))
351 oveq2 7423 . . . . . . . . . . . . . . 15 (𝑧 = (𝐹𝑤) → (𝑥𝐽𝑧) = (𝑥𝐽(𝐹𝑤)))
352351eleq2d 2815 . . . . . . . . . . . . . 14 (𝑧 = (𝐹𝑤) → (𝑦 ∈ (𝑥𝐽𝑧) ↔ 𝑦 ∈ (𝑥𝐽(𝐹𝑤))))
353 oveq2 7423 . . . . . . . . . . . . . . 15 (𝑧 = (𝐹𝑤) → (𝑦𝐸𝑧) = (𝑦𝐸(𝐹𝑤)))
354353eqeq1d 2730 . . . . . . . . . . . . . 14 (𝑧 = (𝐹𝑤) → ((𝑦𝐸𝑧) = (𝑎𝐸𝑏) ↔ (𝑦𝐸(𝐹𝑤)) = (𝑎𝐸𝑏)))
355352, 354anbi12d 631 . . . . . . . . . . . . 13 (𝑧 = (𝐹𝑤) → ((𝑦 ∈ (𝑥𝐽𝑧) ∧ (𝑦𝐸𝑧) = (𝑎𝐸𝑏)) ↔ (𝑦 ∈ (𝑥𝐽(𝐹𝑤)) ∧ (𝑦𝐸(𝐹𝑤)) = (𝑎𝐸𝑏))))
356355adantl 481 . . . . . . . . . . . 12 (((𝜑𝑤𝑃) ∧ 𝑧 = (𝐹𝑤)) → ((𝑦 ∈ (𝑥𝐽𝑧) ∧ (𝑦𝐸𝑧) = (𝑎𝐸𝑏)) ↔ (𝑦 ∈ (𝑥𝐽(𝐹𝑤)) ∧ (𝑦𝐸(𝐹𝑤)) = (𝑎𝐸𝑏))))
357336, 356rspcedv 3601 . . . . . . . . . . 11 ((𝜑𝑤𝑃) → ((𝑦 ∈ (𝑥𝐽(𝐹𝑤)) ∧ (𝑦𝐸(𝐹𝑤)) = (𝑎𝐸𝑏)) → ∃𝑧𝐵 (𝑦 ∈ (𝑥𝐽𝑧) ∧ (𝑦𝐸𝑧) = (𝑎𝐸𝑏))))
358357imp 406 . . . . . . . . . 10 (((𝜑𝑤𝑃) ∧ (𝑦 ∈ (𝑥𝐽(𝐹𝑤)) ∧ (𝑦𝐸(𝐹𝑤)) = (𝑎𝐸𝑏))) → ∃𝑧𝐵 (𝑦 ∈ (𝑥𝐽𝑧) ∧ (𝑦𝐸𝑧) = (𝑎𝐸𝑏)))
359325, 326, 340, 350, 358syl22anc 838 . . . . . . . . 9 (((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑎𝐵𝑏𝐵)) ∧ 𝑤𝑃) ∧ ((𝐹𝑦) ∈ ((𝐹𝑥)𝐼𝑤) ∧ ((𝐹𝑦)𝐷𝑤) = ((𝐹𝑎)𝐷(𝐹𝑏)))) → ∃𝑧𝐵 (𝑦 ∈ (𝑥𝐽𝑧) ∧ (𝑦𝐸𝑧) = (𝑎𝐸𝑏)))
3607adantr 480 . . . . . . . . . 10 (((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑎𝐵𝑏𝐵)) → 𝐺 ∈ TarskiG)
36113adantr 480 . . . . . . . . . 10 (((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑎𝐵𝑏𝐵)) → (𝐹𝑥) ∈ 𝑃)
36215adantr 480 . . . . . . . . . 10 (((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑎𝐵𝑏𝐵)) → (𝐹𝑦) ∈ 𝑃)
36311adantr 480 . . . . . . . . . . 11 (((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑎𝐵𝑏𝐵)) → 𝐹:𝐵𝑃)
364363, 345ffvelcdmd 7090 . . . . . . . . . 10 (((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑎𝐵𝑏𝐵)) → (𝐹𝑎) ∈ 𝑃)
365363, 347ffvelcdmd 7090 . . . . . . . . . 10 (((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑎𝐵𝑏𝐵)) → (𝐹𝑏) ∈ 𝑃)
3663, 4, 5, 360, 361, 362, 364, 365axtgsegcon 28262 . . . . . . . . 9 (((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑎𝐵𝑏𝐵)) → ∃𝑤𝑃 ((𝐹𝑦) ∈ ((𝐹𝑥)𝐼𝑤) ∧ ((𝐹𝑦)𝐷𝑤) = ((𝐹𝑎)𝐷(𝐹𝑏))))
367359, 366r19.29a 3158 . . . . . . . 8 (((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑎𝐵𝑏𝐵)) → ∃𝑧𝐵 (𝑦 ∈ (𝑥𝐽𝑧) ∧ (𝑦𝐸𝑧) = (𝑎𝐸𝑏)))
368367ralrimivva 3196 . . . . . . 7 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → ∀𝑎𝐵𝑏𝐵𝑧𝐵 (𝑦 ∈ (𝑥𝐽𝑧) ∧ (𝑦𝐸𝑧) = (𝑎𝐸𝑏)))
369368ralrimivva 3196 . . . . . 6 (𝜑 → ∀𝑥𝐵𝑦𝐵𝑎𝐵𝑏𝐵𝑧𝐵 (𝑦 ∈ (𝑥𝐽𝑧) ∧ (𝑦𝐸𝑧) = (𝑎𝐸𝑏)))
3702, 324, 369jca32 515 . . . . 5 (𝜑 → (𝐻 ∈ V ∧ (∀𝑥𝐵𝑦𝐵𝑧𝐵𝑢𝐵𝑎𝐵𝑏𝐵𝑐𝐵𝑣𝐵 (((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣)))) → (𝑧𝐸𝑢) = (𝑐𝐸𝑣)) ∧ ∀𝑥𝐵𝑦𝐵𝑎𝐵𝑏𝐵𝑧𝐵 (𝑦 ∈ (𝑥𝐽𝑧) ∧ (𝑦𝐸𝑧) = (𝑎𝐸𝑏)))))
37117, 18, 19istrkgcb 28254 . . . . 5 (𝐻 ∈ TarskiGCB ↔ (𝐻 ∈ V ∧ (∀𝑥𝐵𝑦𝐵𝑧𝐵𝑢𝐵𝑎𝐵𝑏𝐵𝑐𝐵𝑣𝐵 (((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣)))) → (𝑧𝐸𝑢) = (𝑐𝐸𝑣)) ∧ ∀𝑥𝐵𝑦𝐵𝑎𝐵𝑏𝐵𝑧𝐵 (𝑦 ∈ (𝑥𝐽𝑧) ∧ (𝑦𝐸𝑧) = (𝑎𝐸𝑏)))))
372370, 371sylibr 233 . . . 4 (𝜑𝐻 ∈ TarskiGCB)
373 f1otrg.l . . . . 5 (𝜑 → (LineG‘𝐻) = (𝑥𝐵, 𝑦 ∈ (𝐵 ∖ {𝑥}) ↦ {𝑧𝐵 ∣ (𝑧 ∈ (𝑥𝐽𝑦) ∨ 𝑥 ∈ (𝑧𝐽𝑦) ∨ 𝑦 ∈ (𝑥𝐽𝑧))}))
37417, 18, 19istrkgl 28256 . . . . 5 (𝐻 ∈ {𝑓[(Base‘𝑓) / 𝑝][(Itv‘𝑓) / 𝑖](LineG‘𝑓) = (𝑥𝑝, 𝑦 ∈ (𝑝 ∖ {𝑥}) ↦ {𝑧𝑝 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})} ↔ (𝐻 ∈ V ∧ (LineG‘𝐻) = (𝑥𝐵, 𝑦 ∈ (𝐵 ∖ {𝑥}) ↦ {𝑧𝐵 ∣ (𝑧 ∈ (𝑥𝐽𝑦) ∨ 𝑥 ∈ (𝑧𝐽𝑦) ∨ 𝑦 ∈ (𝑥𝐽𝑧))})))
3752, 373, 374sylanbrc 582 . . . 4 (𝜑𝐻 ∈ {𝑓[(Base‘𝑓) / 𝑝][(Itv‘𝑓) / 𝑖](LineG‘𝑓) = (𝑥𝑝, 𝑦 ∈ (𝑝 ∖ {𝑥}) ↦ {𝑧𝑝 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})})
376372, 375elind 4191 . . 3 (𝜑𝐻 ∈ (TarskiGCB ∩ {𝑓[(Base‘𝑓) / 𝑝][(Itv‘𝑓) / 𝑖](LineG‘𝑓) = (𝑥𝑝, 𝑦 ∈ (𝑝 ∖ {𝑥}) ↦ {𝑧𝑝 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})}))
377252, 376elind 4191 . 2 (𝜑𝐻 ∈ ((TarskiGC ∩ TarskiGB) ∩ (TarskiGCB ∩ {𝑓[(Base‘𝑓) / 𝑝][(Itv‘𝑓) / 𝑖](LineG‘𝑓) = (𝑥𝑝, 𝑦 ∈ (𝑝 ∖ {𝑥}) ↦ {𝑧𝑝 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})})))
378 df-trkg 28251 . 2 TarskiG = ((TarskiGC ∩ TarskiGB) ∩ (TarskiGCB ∩ {𝑓[(Base‘𝑓) / 𝑝][(Itv‘𝑓) / 𝑖](LineG‘𝑓) = (𝑥𝑝, 𝑦 ∈ (𝑝 ∖ {𝑥}) ↦ {𝑧𝑝 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})}))
379377, 378eleqtrrdi 2840 1 (𝜑𝐻 ∈ TarskiG)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 395  w3o 1084  w3a 1085   = wceq 1534  wcel 2099  {cab 2705  wne 2936  wral 3057  wrex 3066  {crab 3428  Vcvv 3470  [wsbc 3775  cdif 3942  cin 3944  wss 3945  𝒫 cpw 4599  {csn 4625  ccnv 5672  ran crn 5674  cima 5676   Fn wfn 6538  wf 6539  1-1wf1 6540  ontowfo 6541  1-1-ontowf1o 6542  cfv 6543  (class class class)co 7415  cmpo 7417  Basecbs 17174  distcds 17236  TarskiGcstrkg 28225  TarskiGCcstrkgc 28226  TarskiGBcstrkgb 28227  TarskiGCBcstrkgcb 28228  Itvcitv 28231  LineGclng 28232
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2167  ax-ext 2699  ax-sep 5294  ax-nul 5301  ax-pr 5424
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3or 1086  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2530  df-eu 2559  df-clab 2706  df-cleq 2720  df-clel 2806  df-ne 2937  df-ral 3058  df-rex 3067  df-rab 3429  df-v 3472  df-sbc 3776  df-dif 3948  df-un 3950  df-in 3952  df-ss 3962  df-nul 4320  df-if 4526  df-pw 4601  df-sn 4626  df-pr 4628  df-op 4632  df-uni 4905  df-br 5144  df-opab 5206  df-id 5571  df-xp 5679  df-rel 5680  df-cnv 5681  df-co 5682  df-dm 5683  df-rn 5684  df-res 5685  df-ima 5686  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-ov 7418  df-oprab 7419  df-mpo 7420  df-trkgc 28246  df-trkgb 28247  df-trkgcb 28248  df-trkg 28251
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator