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

Theorem f1otrg 27813
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 3465 . . . . 5 (𝜑𝐻 ∈ V)
3 f1otrkg.p . . . . . . . . 9 𝑃 = (Base‘𝐺)
4 f1otrkg.d . . . . . . . . 9 𝐷 = (dist‘𝐺)
5 f1otrkg.i . . . . . . . . 9 𝐼 = (Itv‘𝐺)
6 f1otrg.g . . . . . . . . . 10 (𝜑𝐺 ∈ TarskiG)
76adantr 481 . . . . . . . . 9 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → 𝐺 ∈ TarskiG)
8 f1otrkg.f . . . . . . . . . . . 12 (𝜑𝐹:𝐵1-1-onto𝑃)
9 f1of 6784 . . . . . . . . . . . 12 (𝐹:𝐵1-1-onto𝑃𝐹:𝐵𝑃)
108, 9syl 17 . . . . . . . . . . 11 (𝜑𝐹:𝐵𝑃)
1110adantr 481 . . . . . . . . . 10 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → 𝐹:𝐵𝑃)
12 simprl 769 . . . . . . . . . 10 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → 𝑥𝐵)
1311, 12ffvelcdmd 7036 . . . . . . . . 9 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → (𝐹𝑥) ∈ 𝑃)
14 simprr 771 . . . . . . . . . 10 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → 𝑦𝐵)
1511, 14ffvelcdmd 7036 . . . . . . . . 9 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → (𝐹𝑦) ∈ 𝑃)
163, 4, 5, 7, 13, 15axtgcgrrflx 27404 . . . . . . . 8 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → ((𝐹𝑥)𝐷(𝐹𝑦)) = ((𝐹𝑦)𝐷(𝐹𝑥)))
17 f1otrkg.b . . . . . . . . 9 𝐵 = (Base‘𝐻)
18 f1otrkg.e . . . . . . . . 9 𝐸 = (dist‘𝐻)
19 f1otrkg.j . . . . . . . . 9 𝐽 = (Itv‘𝐻)
208adantr 481 . . . . . . . . 9 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → 𝐹:𝐵1-1-onto𝑃)
21 f1otrkg.1 . . . . . . . . . 10 ((𝜑 ∧ (𝑒𝐵𝑓𝐵)) → (𝑒𝐸𝑓) = ((𝐹𝑒)𝐷(𝐹𝑓)))
2221adantlr 713 . . . . . . . . 9 (((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑒𝐵𝑓𝐵)) → (𝑒𝐸𝑓) = ((𝐹𝑒)𝐷(𝐹𝑓)))
23 f1otrkg.2 . . . . . . . . . 10 ((𝜑 ∧ (𝑒𝐵𝑓𝐵𝑔𝐵)) → (𝑔 ∈ (𝑒𝐽𝑓) ↔ (𝐹𝑔) ∈ ((𝐹𝑒)𝐼(𝐹𝑓))))
2423adantlr 713 . . . . . . . . 9 (((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑒𝐵𝑓𝐵𝑔𝐵)) → (𝑔 ∈ (𝑒𝐽𝑓) ↔ (𝐹𝑔) ∈ ((𝐹𝑒)𝐼(𝐹𝑓))))
253, 4, 5, 17, 18, 19, 20, 22, 24, 12, 14f1otrgds 27811 . . . . . . . 8 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → (𝑥𝐸𝑦) = ((𝐹𝑥)𝐷(𝐹𝑦)))
263, 4, 5, 17, 18, 19, 20, 22, 24, 14, 12f1otrgds 27811 . . . . . . . 8 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → (𝑦𝐸𝑥) = ((𝐹𝑦)𝐷(𝐹𝑥)))
2716, 25, 263eqtr4d 2786 . . . . . . 7 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → (𝑥𝐸𝑦) = (𝑦𝐸𝑥))
2827ralrimivva 3197 . . . . . 6 (𝜑 → ∀𝑥𝐵𝑦𝐵 (𝑥𝐸𝑦) = (𝑦𝐸𝑥))
29 f1of1 6783 . . . . . . . . . . 11 (𝐹:𝐵1-1-onto𝑃𝐹:𝐵1-1𝑃)
308, 29syl 17 . . . . . . . . . 10 (𝜑𝐹:𝐵1-1𝑃)
31303ad2ant1 1133 . . . . . . . . 9 ((𝜑 ∧ (𝑥𝐵𝑦𝐵𝑧𝐵) ∧ (𝑥𝐸𝑦) = (𝑧𝐸𝑧)) → 𝐹:𝐵1-1𝑃)
32 simp21 1206 . . . . . . . . . 10 ((𝜑 ∧ (𝑥𝐵𝑦𝐵𝑧𝐵) ∧ (𝑥𝐸𝑦) = (𝑧𝐸𝑧)) → 𝑥𝐵)
33 simp22 1207 . . . . . . . . . 10 ((𝜑 ∧ (𝑥𝐵𝑦𝐵𝑧𝐵) ∧ (𝑥𝐸𝑦) = (𝑧𝐸𝑧)) → 𝑦𝐵)
3432, 33jca 512 . . . . . . . . 9 ((𝜑 ∧ (𝑥𝐵𝑦𝐵𝑧𝐵) ∧ (𝑥𝐸𝑦) = (𝑧𝐸𝑧)) → (𝑥𝐵𝑦𝐵))
3563ad2ant1 1133 . . . . . . . . . 10 ((𝜑 ∧ (𝑥𝐵𝑦𝐵𝑧𝐵) ∧ (𝑥𝐸𝑦) = (𝑧𝐸𝑧)) → 𝐺 ∈ TarskiG)
36103ad2ant1 1133 . . . . . . . . . . 11 ((𝜑 ∧ (𝑥𝐵𝑦𝐵𝑧𝐵) ∧ (𝑥𝐸𝑦) = (𝑧𝐸𝑧)) → 𝐹:𝐵𝑃)
3736, 32ffvelcdmd 7036 . . . . . . . . . 10 ((𝜑 ∧ (𝑥𝐵𝑦𝐵𝑧𝐵) ∧ (𝑥𝐸𝑦) = (𝑧𝐸𝑧)) → (𝐹𝑥) ∈ 𝑃)
3836, 33ffvelcdmd 7036 . . . . . . . . . 10 ((𝜑 ∧ (𝑥𝐵𝑦𝐵𝑧𝐵) ∧ (𝑥𝐸𝑦) = (𝑧𝐸𝑧)) → (𝐹𝑦) ∈ 𝑃)
39 simp23 1208 . . . . . . . . . . 11 ((𝜑 ∧ (𝑥𝐵𝑦𝐵𝑧𝐵) ∧ (𝑥𝐸𝑦) = (𝑧𝐸𝑧)) → 𝑧𝐵)
4036, 39ffvelcdmd 7036 . . . . . . . . . 10 ((𝜑 ∧ (𝑥𝐵𝑦𝐵𝑧𝐵) ∧ (𝑥𝐸𝑦) = (𝑧𝐸𝑧)) → (𝐹𝑧) ∈ 𝑃)
41 simp3 1138 . . . . . . . . . . 11 ((𝜑 ∧ (𝑥𝐵𝑦𝐵𝑧𝐵) ∧ (𝑥𝐸𝑦) = (𝑧𝐸𝑧)) → (𝑥𝐸𝑦) = (𝑧𝐸𝑧))
4283ad2ant1 1133 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑥𝐵𝑦𝐵𝑧𝐵) ∧ (𝑥𝐸𝑦) = (𝑧𝐸𝑧)) → 𝐹:𝐵1-1-onto𝑃)
43213ad2antl1 1185 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑥𝐵𝑦𝐵𝑧𝐵) ∧ (𝑥𝐸𝑦) = (𝑧𝐸𝑧)) ∧ (𝑒𝐵𝑓𝐵)) → (𝑒𝐸𝑓) = ((𝐹𝑒)𝐷(𝐹𝑓)))
44233ad2antl1 1185 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑥𝐵𝑦𝐵𝑧𝐵) ∧ (𝑥𝐸𝑦) = (𝑧𝐸𝑧)) ∧ (𝑒𝐵𝑓𝐵𝑔𝐵)) → (𝑔 ∈ (𝑒𝐽𝑓) ↔ (𝐹𝑔) ∈ ((𝐹𝑒)𝐼(𝐹𝑓))))
453, 4, 5, 17, 18, 19, 42, 43, 44, 32, 33f1otrgds 27811 . . . . . . . . . . 11 ((𝜑 ∧ (𝑥𝐵𝑦𝐵𝑧𝐵) ∧ (𝑥𝐸𝑦) = (𝑧𝐸𝑧)) → (𝑥𝐸𝑦) = ((𝐹𝑥)𝐷(𝐹𝑦)))
463, 4, 5, 17, 18, 19, 42, 43, 44, 39, 39f1otrgds 27811 . . . . . . . . . . 11 ((𝜑 ∧ (𝑥𝐵𝑦𝐵𝑧𝐵) ∧ (𝑥𝐸𝑦) = (𝑧𝐸𝑧)) → (𝑧𝐸𝑧) = ((𝐹𝑧)𝐷(𝐹𝑧)))
4741, 45, 463eqtr3d 2784 . . . . . . . . . 10 ((𝜑 ∧ (𝑥𝐵𝑦𝐵𝑧𝐵) ∧ (𝑥𝐸𝑦) = (𝑧𝐸𝑧)) → ((𝐹𝑥)𝐷(𝐹𝑦)) = ((𝐹𝑧)𝐷(𝐹𝑧)))
483, 4, 5, 35, 37, 38, 40, 47axtgcgrid 27405 . . . . . . . . 9 ((𝜑 ∧ (𝑥𝐵𝑦𝐵𝑧𝐵) ∧ (𝑥𝐸𝑦) = (𝑧𝐸𝑧)) → (𝐹𝑥) = (𝐹𝑦))
49 f1veqaeq 7204 . . . . . . . . . 10 ((𝐹:𝐵1-1𝑃 ∧ (𝑥𝐵𝑦𝐵)) → ((𝐹𝑥) = (𝐹𝑦) → 𝑥 = 𝑦))
5049imp 407 . . . . . . . . 9 (((𝐹:𝐵1-1𝑃 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝐹𝑥) = (𝐹𝑦)) → 𝑥 = 𝑦)
5131, 34, 48, 50syl21anc 836 . . . . . . . 8 ((𝜑 ∧ (𝑥𝐵𝑦𝐵𝑧𝐵) ∧ (𝑥𝐸𝑦) = (𝑧𝐸𝑧)) → 𝑥 = 𝑦)
52513expia 1121 . . . . . . 7 ((𝜑 ∧ (𝑥𝐵𝑦𝐵𝑧𝐵)) → ((𝑥𝐸𝑦) = (𝑧𝐸𝑧) → 𝑥 = 𝑦))
5352ralrimivvva 3200 . . . . . 6 (𝜑 → ∀𝑥𝐵𝑦𝐵𝑧𝐵 ((𝑥𝐸𝑦) = (𝑧𝐸𝑧) → 𝑥 = 𝑦))
5428, 53jca 512 . . . . 5 (𝜑 → (∀𝑥𝐵𝑦𝐵 (𝑥𝐸𝑦) = (𝑦𝐸𝑥) ∧ ∀𝑥𝐵𝑦𝐵𝑧𝐵 ((𝑥𝐸𝑦) = (𝑧𝐸𝑧) → 𝑥 = 𝑦)))
5517, 18, 19istrkgc 27396 . . . . 5 (𝐻 ∈ TarskiGC ↔ (𝐻 ∈ V ∧ (∀𝑥𝐵𝑦𝐵 (𝑥𝐸𝑦) = (𝑦𝐸𝑥) ∧ ∀𝑥𝐵𝑦𝐵𝑧𝐵 ((𝑥𝐸𝑦) = (𝑧𝐸𝑧) → 𝑥 = 𝑦))))
562, 54, 55sylanbrc 583 . . . 4 (𝜑𝐻 ∈ TarskiGC)
5783ad2ant1 1133 . . . . . . . . . 10 ((𝜑 ∧ (𝑥𝐵𝑦𝐵) ∧ 𝑦 ∈ (𝑥𝐽𝑥)) → 𝐹:𝐵1-1-onto𝑃)
5857, 29syl 17 . . . . . . . . 9 ((𝜑 ∧ (𝑥𝐵𝑦𝐵) ∧ 𝑦 ∈ (𝑥𝐽𝑥)) → 𝐹:𝐵1-1𝑃)
59 simp2 1137 . . . . . . . . 9 ((𝜑 ∧ (𝑥𝐵𝑦𝐵) ∧ 𝑦 ∈ (𝑥𝐽𝑥)) → (𝑥𝐵𝑦𝐵))
6063ad2ant1 1133 . . . . . . . . . 10 ((𝜑 ∧ (𝑥𝐵𝑦𝐵) ∧ 𝑦 ∈ (𝑥𝐽𝑥)) → 𝐺 ∈ TarskiG)
61133adant3 1132 . . . . . . . . . 10 ((𝜑 ∧ (𝑥𝐵𝑦𝐵) ∧ 𝑦 ∈ (𝑥𝐽𝑥)) → (𝐹𝑥) ∈ 𝑃)
62153adant3 1132 . . . . . . . . . 10 ((𝜑 ∧ (𝑥𝐵𝑦𝐵) ∧ 𝑦 ∈ (𝑥𝐽𝑥)) → (𝐹𝑦) ∈ 𝑃)
63 simp3 1138 . . . . . . . . . . 11 ((𝜑 ∧ (𝑥𝐵𝑦𝐵) ∧ 𝑦 ∈ (𝑥𝐽𝑥)) → 𝑦 ∈ (𝑥𝐽𝑥))
64213ad2antl1 1185 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑥𝐵𝑦𝐵) ∧ 𝑦 ∈ (𝑥𝐽𝑥)) ∧ (𝑒𝐵𝑓𝐵)) → (𝑒𝐸𝑓) = ((𝐹𝑒)𝐷(𝐹𝑓)))
65233ad2antl1 1185 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑥𝐵𝑦𝐵) ∧ 𝑦 ∈ (𝑥𝐽𝑥)) ∧ (𝑒𝐵𝑓𝐵𝑔𝐵)) → (𝑔 ∈ (𝑒𝐽𝑓) ↔ (𝐹𝑔) ∈ ((𝐹𝑒)𝐼(𝐹𝑓))))
66123adant3 1132 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑥𝐵𝑦𝐵) ∧ 𝑦 ∈ (𝑥𝐽𝑥)) → 𝑥𝐵)
67143adant3 1132 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑥𝐵𝑦𝐵) ∧ 𝑦 ∈ (𝑥𝐽𝑥)) → 𝑦𝐵)
683, 4, 5, 17, 18, 19, 57, 64, 65, 66, 66, 67f1otrgitv 27812 . . . . . . . . . . 11 ((𝜑 ∧ (𝑥𝐵𝑦𝐵) ∧ 𝑦 ∈ (𝑥𝐽𝑥)) → (𝑦 ∈ (𝑥𝐽𝑥) ↔ (𝐹𝑦) ∈ ((𝐹𝑥)𝐼(𝐹𝑥))))
6963, 68mpbid 231 . . . . . . . . . 10 ((𝜑 ∧ (𝑥𝐵𝑦𝐵) ∧ 𝑦 ∈ (𝑥𝐽𝑥)) → (𝐹𝑦) ∈ ((𝐹𝑥)𝐼(𝐹𝑥)))
703, 4, 5, 60, 61, 62, 69axtgbtwnid 27408 . . . . . . . . 9 ((𝜑 ∧ (𝑥𝐵𝑦𝐵) ∧ 𝑦 ∈ (𝑥𝐽𝑥)) → (𝐹𝑥) = (𝐹𝑦))
7158, 59, 70, 50syl21anc 836 . . . . . . . 8 ((𝜑 ∧ (𝑥𝐵𝑦𝐵) ∧ 𝑦 ∈ (𝑥𝐽𝑥)) → 𝑥 = 𝑦)
72713expia 1121 . . . . . . 7 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → (𝑦 ∈ (𝑥𝐽𝑥) → 𝑥 = 𝑦))
7372ralrimivva 3197 . . . . . 6 (𝜑 → ∀𝑥𝐵𝑦𝐵 (𝑦 ∈ (𝑥𝐽𝑥) → 𝑥 = 𝑦))
74 f1ocnv 6796 . . . . . . . . . . . . . 14 (𝐹:𝐵1-1-onto𝑃𝐹:𝑃1-1-onto𝐵)
75 f1of 6784 . . . . . . . . . . . . . 14 (𝐹:𝑃1-1-onto𝐵𝐹:𝑃𝐵)
768, 74, 753syl 18 . . . . . . . . . . . . 13 (𝜑𝐹:𝑃𝐵)
7776ad5antr 732 . . . . . . . . . . . 12 ((((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐𝑃) ∧ (𝑐 ∈ ((𝐹𝑢)𝐼(𝐹𝑦)) ∧ 𝑐 ∈ ((𝐹𝑣)𝐼(𝐹𝑥)))) → 𝐹:𝑃𝐵)
78 simplr 767 . . . . . . . . . . . 12 ((((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐𝑃) ∧ (𝑐 ∈ ((𝐹𝑢)𝐼(𝐹𝑦)) ∧ 𝑐 ∈ ((𝐹𝑣)𝐼(𝐹𝑥)))) → 𝑐𝑃)
7977, 78ffvelcdmd 7036 . . . . . . . . . . 11 ((((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐𝑃) ∧ (𝑐 ∈ ((𝐹𝑢)𝐼(𝐹𝑦)) ∧ 𝑐 ∈ ((𝐹𝑣)𝐼(𝐹𝑥)))) → (𝐹𝑐) ∈ 𝐵)
80 simpr 485 . . . . . . . . . . . . 13 (((((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐𝑃) ∧ (𝑐 ∈ ((𝐹𝑢)𝐼(𝐹𝑦)) ∧ 𝑐 ∈ ((𝐹𝑣)𝐼(𝐹𝑥)))) ∧ 𝑎 = (𝐹𝑐)) → 𝑎 = (𝐹𝑐))
8180eleq1d 2822 . . . . . . . . . . . 12 (((((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐𝑃) ∧ (𝑐 ∈ ((𝐹𝑢)𝐼(𝐹𝑦)) ∧ 𝑐 ∈ ((𝐹𝑣)𝐼(𝐹𝑥)))) ∧ 𝑎 = (𝐹𝑐)) → (𝑎 ∈ (𝑢𝐽𝑦) ↔ (𝐹𝑐) ∈ (𝑢𝐽𝑦)))
8280eleq1d 2822 . . . . . . . . . . . 12 (((((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐𝑃) ∧ (𝑐 ∈ ((𝐹𝑢)𝐼(𝐹𝑦)) ∧ 𝑐 ∈ ((𝐹𝑣)𝐼(𝐹𝑥)))) ∧ 𝑎 = (𝐹𝑐)) → (𝑎 ∈ (𝑣𝐽𝑥) ↔ (𝐹𝑐) ∈ (𝑣𝐽𝑥)))
8381, 82anbi12d 631 . . . . . . . . . . 11 (((((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐𝑃) ∧ (𝑐 ∈ ((𝐹𝑢)𝐼(𝐹𝑦)) ∧ 𝑐 ∈ ((𝐹𝑣)𝐼(𝐹𝑥)))) ∧ 𝑎 = (𝐹𝑐)) → ((𝑎 ∈ (𝑢𝐽𝑦) ∧ 𝑎 ∈ (𝑣𝐽𝑥)) ↔ ((𝐹𝑐) ∈ (𝑢𝐽𝑦) ∧ (𝐹𝑐) ∈ (𝑣𝐽𝑥))))
84 simprl 769 . . . . . . . . . . . . . 14 ((((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐𝑃) ∧ (𝑐 ∈ ((𝐹𝑢)𝐼(𝐹𝑦)) ∧ 𝑐 ∈ ((𝐹𝑣)𝐼(𝐹𝑥)))) → 𝑐 ∈ ((𝐹𝑢)𝐼(𝐹𝑦)))
8520ad2antrr 724 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) → 𝐹:𝐵1-1-onto𝑃)
8685ad2antrr 724 . . . . . . . . . . . . . . 15 ((((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐𝑃) ∧ (𝑐 ∈ ((𝐹𝑢)𝐼(𝐹𝑦)) ∧ 𝑐 ∈ ((𝐹𝑣)𝐼(𝐹𝑥)))) → 𝐹:𝐵1-1-onto𝑃)
87 f1ocnvfv2 7223 . . . . . . . . . . . . . . . 16 ((𝐹:𝐵1-1-onto𝑃𝑐𝑃) → (𝐹‘(𝐹𝑐)) = 𝑐)
8887eleq1d 2822 . . . . . . . . . . . . . . 15 ((𝐹:𝐵1-1-onto𝑃𝑐𝑃) → ((𝐹‘(𝐹𝑐)) ∈ ((𝐹𝑢)𝐼(𝐹𝑦)) ↔ 𝑐 ∈ ((𝐹𝑢)𝐼(𝐹𝑦))))
8986, 78, 88syl2anc 584 . . . . . . . . . . . . . 14 ((((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐𝑃) ∧ (𝑐 ∈ ((𝐹𝑢)𝐼(𝐹𝑦)) ∧ 𝑐 ∈ ((𝐹𝑣)𝐼(𝐹𝑥)))) → ((𝐹‘(𝐹𝑐)) ∈ ((𝐹𝑢)𝐼(𝐹𝑦)) ↔ 𝑐 ∈ ((𝐹𝑢)𝐼(𝐹𝑦))))
9084, 89mpbird 256 . . . . . . . . . . . . 13 ((((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐𝑃) ∧ (𝑐 ∈ ((𝐹𝑢)𝐼(𝐹𝑦)) ∧ 𝑐 ∈ ((𝐹𝑣)𝐼(𝐹𝑥)))) → (𝐹‘(𝐹𝑐)) ∈ ((𝐹𝑢)𝐼(𝐹𝑦)))
9122ad4ant14 750 . . . . . . . . . . . . . . 15 (((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ (𝑒𝐵𝑓𝐵)) → (𝑒𝐸𝑓) = ((𝐹𝑒)𝐷(𝐹𝑓)))
9291ad4ant14 750 . . . . . . . . . . . . . 14 (((((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐𝑃) ∧ (𝑐 ∈ ((𝐹𝑢)𝐼(𝐹𝑦)) ∧ 𝑐 ∈ ((𝐹𝑣)𝐼(𝐹𝑥)))) ∧ (𝑒𝐵𝑓𝐵)) → (𝑒𝐸𝑓) = ((𝐹𝑒)𝐷(𝐹𝑓)))
9324ad4ant14 750 . . . . . . . . . . . . . . 15 (((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ (𝑒𝐵𝑓𝐵𝑔𝐵)) → (𝑔 ∈ (𝑒𝐽𝑓) ↔ (𝐹𝑔) ∈ ((𝐹𝑒)𝐼(𝐹𝑓))))
9493ad4ant14 750 . . . . . . . . . . . . . 14 (((((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐𝑃) ∧ (𝑐 ∈ ((𝐹𝑢)𝐼(𝐹𝑦)) ∧ 𝑐 ∈ ((𝐹𝑣)𝐼(𝐹𝑥)))) ∧ (𝑒𝐵𝑓𝐵𝑔𝐵)) → (𝑔 ∈ (𝑒𝐽𝑓) ↔ (𝐹𝑔) ∈ ((𝐹𝑒)𝐼(𝐹𝑓))))
95 simplr2 1216 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) → 𝑢𝐵)
9695ad2antrr 724 . . . . . . . . . . . . . 14 ((((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐𝑃) ∧ (𝑐 ∈ ((𝐹𝑢)𝐼(𝐹𝑦)) ∧ 𝑐 ∈ ((𝐹𝑣)𝐼(𝐹𝑥)))) → 𝑢𝐵)
9714ad2antrr 724 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) → 𝑦𝐵)
9897ad2antrr 724 . . . . . . . . . . . . . 14 ((((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐𝑃) ∧ (𝑐 ∈ ((𝐹𝑢)𝐼(𝐹𝑦)) ∧ 𝑐 ∈ ((𝐹𝑣)𝐼(𝐹𝑥)))) → 𝑦𝐵)
993, 4, 5, 17, 18, 19, 86, 92, 94, 96, 98, 79f1otrgitv 27812 . . . . . . . . . . . . 13 ((((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐𝑃) ∧ (𝑐 ∈ ((𝐹𝑢)𝐼(𝐹𝑦)) ∧ 𝑐 ∈ ((𝐹𝑣)𝐼(𝐹𝑥)))) → ((𝐹𝑐) ∈ (𝑢𝐽𝑦) ↔ (𝐹‘(𝐹𝑐)) ∈ ((𝐹𝑢)𝐼(𝐹𝑦))))
10090, 99mpbird 256 . . . . . . . . . . . 12 ((((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐𝑃) ∧ (𝑐 ∈ ((𝐹𝑢)𝐼(𝐹𝑦)) ∧ 𝑐 ∈ ((𝐹𝑣)𝐼(𝐹𝑥)))) → (𝐹𝑐) ∈ (𝑢𝐽𝑦))
101 simprr 771 . . . . . . . . . . . . . 14 ((((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐𝑃) ∧ (𝑐 ∈ ((𝐹𝑢)𝐼(𝐹𝑦)) ∧ 𝑐 ∈ ((𝐹𝑣)𝐼(𝐹𝑥)))) → 𝑐 ∈ ((𝐹𝑣)𝐼(𝐹𝑥)))
10287eleq1d 2822 . . . . . . . . . . . . . . 15 ((𝐹:𝐵1-1-onto𝑃𝑐𝑃) → ((𝐹‘(𝐹𝑐)) ∈ ((𝐹𝑣)𝐼(𝐹𝑥)) ↔ 𝑐 ∈ ((𝐹𝑣)𝐼(𝐹𝑥))))
10386, 78, 102syl2anc 584 . . . . . . . . . . . . . 14 ((((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐𝑃) ∧ (𝑐 ∈ ((𝐹𝑢)𝐼(𝐹𝑦)) ∧ 𝑐 ∈ ((𝐹𝑣)𝐼(𝐹𝑥)))) → ((𝐹‘(𝐹𝑐)) ∈ ((𝐹𝑣)𝐼(𝐹𝑥)) ↔ 𝑐 ∈ ((𝐹𝑣)𝐼(𝐹𝑥))))
104101, 103mpbird 256 . . . . . . . . . . . . 13 ((((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐𝑃) ∧ (𝑐 ∈ ((𝐹𝑢)𝐼(𝐹𝑦)) ∧ 𝑐 ∈ ((𝐹𝑣)𝐼(𝐹𝑥)))) → (𝐹‘(𝐹𝑐)) ∈ ((𝐹𝑣)𝐼(𝐹𝑥)))
105 simplr3 1217 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) → 𝑣𝐵)
106105ad2antrr 724 . . . . . . . . . . . . . 14 ((((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐𝑃) ∧ (𝑐 ∈ ((𝐹𝑢)𝐼(𝐹𝑦)) ∧ 𝑐 ∈ ((𝐹𝑣)𝐼(𝐹𝑥)))) → 𝑣𝐵)
10712ad2antrr 724 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) → 𝑥𝐵)
108107ad2antrr 724 . . . . . . . . . . . . . 14 ((((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐𝑃) ∧ (𝑐 ∈ ((𝐹𝑢)𝐼(𝐹𝑦)) ∧ 𝑐 ∈ ((𝐹𝑣)𝐼(𝐹𝑥)))) → 𝑥𝐵)
1093, 4, 5, 17, 18, 19, 86, 92, 94, 106, 108, 79f1otrgitv 27812 . . . . . . . . . . . . 13 ((((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐𝑃) ∧ (𝑐 ∈ ((𝐹𝑢)𝐼(𝐹𝑦)) ∧ 𝑐 ∈ ((𝐹𝑣)𝐼(𝐹𝑥)))) → ((𝐹𝑐) ∈ (𝑣𝐽𝑥) ↔ (𝐹‘(𝐹𝑐)) ∈ ((𝐹𝑣)𝐼(𝐹𝑥))))
110104, 109mpbird 256 . . . . . . . . . . . 12 ((((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐𝑃) ∧ (𝑐 ∈ ((𝐹𝑢)𝐼(𝐹𝑦)) ∧ 𝑐 ∈ ((𝐹𝑣)𝐼(𝐹𝑥)))) → (𝐹𝑐) ∈ (𝑣𝐽𝑥))
111100, 110jca 512 . . . . . . . . . . 11 ((((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐𝑃) ∧ (𝑐 ∈ ((𝐹𝑢)𝐼(𝐹𝑦)) ∧ 𝑐 ∈ ((𝐹𝑣)𝐼(𝐹𝑥)))) → ((𝐹𝑐) ∈ (𝑢𝐽𝑦) ∧ (𝐹𝑐) ∈ (𝑣𝐽𝑥)))
11279, 83, 111rspcedvd 3583 . . . . . . . . . 10 ((((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐𝑃) ∧ (𝑐 ∈ ((𝐹𝑢)𝐼(𝐹𝑦)) ∧ 𝑐 ∈ ((𝐹𝑣)𝐼(𝐹𝑥)))) → ∃𝑎𝐵 (𝑎 ∈ (𝑢𝐽𝑦) ∧ 𝑎 ∈ (𝑣𝐽𝑥)))
1137ad2antrr 724 . . . . . . . . . . 11 ((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) → 𝐺 ∈ TarskiG)
11411ad2antrr 724 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) → 𝐹:𝐵𝑃)
115114, 107ffvelcdmd 7036 . . . . . . . . . . 11 ((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) → (𝐹𝑥) ∈ 𝑃)
116114, 97ffvelcdmd 7036 . . . . . . . . . . 11 ((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) → (𝐹𝑦) ∈ 𝑃)
117 simplr1 1215 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) → 𝑧𝐵)
118114, 117ffvelcdmd 7036 . . . . . . . . . . 11 ((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) → (𝐹𝑧) ∈ 𝑃)
119114, 95ffvelcdmd 7036 . . . . . . . . . . 11 ((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) → (𝐹𝑢) ∈ 𝑃)
120114, 105ffvelcdmd 7036 . . . . . . . . . . 11 ((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) → (𝐹𝑣) ∈ 𝑃)
121 simprl 769 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) → 𝑢 ∈ (𝑥𝐽𝑧))
1223, 4, 5, 17, 18, 19, 85, 91, 93, 107, 117, 95f1otrgitv 27812 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) → (𝑢 ∈ (𝑥𝐽𝑧) ↔ (𝐹𝑢) ∈ ((𝐹𝑥)𝐼(𝐹𝑧))))
123121, 122mpbid 231 . . . . . . . . . . 11 ((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) → (𝐹𝑢) ∈ ((𝐹𝑥)𝐼(𝐹𝑧)))
124 simprr 771 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) → 𝑣 ∈ (𝑦𝐽𝑧))
1253, 4, 5, 17, 18, 19, 85, 91, 93, 97, 117, 105f1otrgitv 27812 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) → (𝑣 ∈ (𝑦𝐽𝑧) ↔ (𝐹𝑣) ∈ ((𝐹𝑦)𝐼(𝐹𝑧))))
126124, 125mpbid 231 . . . . . . . . . . 11 ((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) → (𝐹𝑣) ∈ ((𝐹𝑦)𝐼(𝐹𝑧)))
1273, 4, 5, 113, 115, 116, 118, 119, 120, 123, 126axtgpasch 27409 . . . . . . . . . 10 ((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) → ∃𝑐𝑃 (𝑐 ∈ ((𝐹𝑢)𝐼(𝐹𝑦)) ∧ 𝑐 ∈ ((𝐹𝑣)𝐼(𝐹𝑥))))
128112, 127r19.29a 3159 . . . . . . . . 9 ((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) → ∃𝑎𝐵 (𝑎 ∈ (𝑢𝐽𝑦) ∧ 𝑎 ∈ (𝑣𝐽𝑥)))
129128ex 413 . . . . . . . 8 (((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑢𝐵𝑣𝐵)) → ((𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧)) → ∃𝑎𝐵 (𝑎 ∈ (𝑢𝐽𝑦) ∧ 𝑎 ∈ (𝑣𝐽𝑥))))
130129ralrimivvva 3200 . . . . . . 7 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → ∀𝑧𝐵𝑢𝐵𝑣𝐵 ((𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧)) → ∃𝑎𝐵 (𝑎 ∈ (𝑢𝐽𝑦) ∧ 𝑎 ∈ (𝑣𝐽𝑥))))
131130ralrimivva 3197 . . . . . 6 (𝜑 → ∀𝑥𝐵𝑦𝐵𝑧𝐵𝑢𝐵𝑣𝐵 ((𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧)) → ∃𝑎𝐵 (𝑎 ∈ (𝑢𝐽𝑦) ∧ 𝑎 ∈ (𝑣𝐽𝑥))))
1328ad5antr 732 . . . . . . . . . . . . . . 15 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ 𝑐𝑃) ∧ ∀𝑒 ∈ (𝐹𝑠)∀𝑓 ∈ (𝐹𝑡)𝑐 ∈ (𝑒𝐼𝑓)) ∧ (𝑥𝑠𝑦𝑡)) → 𝐹:𝐵1-1-onto𝑃)
133 simpllr 774 . . . . . . . . . . . . . . 15 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ 𝑐𝑃) ∧ ∀𝑒 ∈ (𝐹𝑠)∀𝑓 ∈ (𝐹𝑡)𝑐 ∈ (𝑒𝐼𝑓)) ∧ (𝑥𝑠𝑦𝑡)) → 𝑐𝑃)
134132, 133, 87syl2anc 584 . . . . . . . . . . . . . 14 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ 𝑐𝑃) ∧ ∀𝑒 ∈ (𝐹𝑠)∀𝑓 ∈ (𝐹𝑡)𝑐 ∈ (𝑒𝐼𝑓)) ∧ (𝑥𝑠𝑦𝑡)) → (𝐹‘(𝐹𝑐)) = 𝑐)
135 ffn 6668 . . . . . . . . . . . . . . . . 17 (𝐹:𝐵𝑃𝐹 Fn 𝐵)
136132, 9, 1353syl 18 . . . . . . . . . . . . . . . 16 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ 𝑐𝑃) ∧ ∀𝑒 ∈ (𝐹𝑠)∀𝑓 ∈ (𝐹𝑡)𝑐 ∈ (𝑒𝐼𝑓)) ∧ (𝑥𝑠𝑦𝑡)) → 𝐹 Fn 𝐵)
137 simp-4r 782 . . . . . . . . . . . . . . . . . . 19 (((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ 𝑐𝑃) ∧ (𝑥𝑠𝑦𝑡)) → (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵))
138137simpld 495 . . . . . . . . . . . . . . . . . 18 (((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ 𝑐𝑃) ∧ (𝑥𝑠𝑦𝑡)) → 𝑠 ∈ 𝒫 𝐵)
139138elpwid 4569 . . . . . . . . . . . . . . . . 17 (((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ 𝑐𝑃) ∧ (𝑥𝑠𝑦𝑡)) → 𝑠𝐵)
140139adantlr 713 . . . . . . . . . . . . . . . 16 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ 𝑐𝑃) ∧ ∀𝑒 ∈ (𝐹𝑠)∀𝑓 ∈ (𝐹𝑡)𝑐 ∈ (𝑒𝐼𝑓)) ∧ (𝑥𝑠𝑦𝑡)) → 𝑠𝐵)
141 simprl 769 . . . . . . . . . . . . . . . 16 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ 𝑐𝑃) ∧ ∀𝑒 ∈ (𝐹𝑠)∀𝑓 ∈ (𝐹𝑡)𝑐 ∈ (𝑒𝐼𝑓)) ∧ (𝑥𝑠𝑦𝑡)) → 𝑥𝑠)
142 fnfvima 7183 . . . . . . . . . . . . . . . 16 ((𝐹 Fn 𝐵𝑠𝐵𝑥𝑠) → (𝐹𝑥) ∈ (𝐹𝑠))
143136, 140, 141, 142syl3anc 1371 . . . . . . . . . . . . . . 15 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ 𝑐𝑃) ∧ ∀𝑒 ∈ (𝐹𝑠)∀𝑓 ∈ (𝐹𝑡)𝑐 ∈ (𝑒𝐼𝑓)) ∧ (𝑥𝑠𝑦𝑡)) → (𝐹𝑥) ∈ (𝐹𝑠))
144137simprd 496 . . . . . . . . . . . . . . . . . 18 (((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ 𝑐𝑃) ∧ (𝑥𝑠𝑦𝑡)) → 𝑡 ∈ 𝒫 𝐵)
145144elpwid 4569 . . . . . . . . . . . . . . . . 17 (((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ 𝑐𝑃) ∧ (𝑥𝑠𝑦𝑡)) → 𝑡𝐵)
146145adantlr 713 . . . . . . . . . . . . . . . 16 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ 𝑐𝑃) ∧ ∀𝑒 ∈ (𝐹𝑠)∀𝑓 ∈ (𝐹𝑡)𝑐 ∈ (𝑒𝐼𝑓)) ∧ (𝑥𝑠𝑦𝑡)) → 𝑡𝐵)
147 simprr 771 . . . . . . . . . . . . . . . 16 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ 𝑐𝑃) ∧ ∀𝑒 ∈ (𝐹𝑠)∀𝑓 ∈ (𝐹𝑡)𝑐 ∈ (𝑒𝐼𝑓)) ∧ (𝑥𝑠𝑦𝑡)) → 𝑦𝑡)
148 fnfvima 7183 . . . . . . . . . . . . . . . 16 ((𝐹 Fn 𝐵𝑡𝐵𝑦𝑡) → (𝐹𝑦) ∈ (𝐹𝑡))
149136, 146, 147, 148syl3anc 1371 . . . . . . . . . . . . . . 15 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ 𝑐𝑃) ∧ ∀𝑒 ∈ (𝐹𝑠)∀𝑓 ∈ (𝐹𝑡)𝑐 ∈ (𝑒𝐼𝑓)) ∧ (𝑥𝑠𝑦𝑡)) → (𝐹𝑦) ∈ (𝐹𝑡))
150 simplr 767 . . . . . . . . . . . . . . 15 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ 𝑐𝑃) ∧ ∀𝑒 ∈ (𝐹𝑠)∀𝑓 ∈ (𝐹𝑡)𝑐 ∈ (𝑒𝐼𝑓)) ∧ (𝑥𝑠𝑦𝑡)) → ∀𝑒 ∈ (𝐹𝑠)∀𝑓 ∈ (𝐹𝑡)𝑐 ∈ (𝑒𝐼𝑓))
151 oveq1 7364 . . . . . . . . . . . . . . . . 17 (𝑒 = (𝐹𝑥) → (𝑒𝐼𝑓) = ((𝐹𝑥)𝐼𝑓))
152151eleq2d 2823 . . . . . . . . . . . . . . . 16 (𝑒 = (𝐹𝑥) → (𝑐 ∈ (𝑒𝐼𝑓) ↔ 𝑐 ∈ ((𝐹𝑥)𝐼𝑓)))
153 oveq2 7365 . . . . . . . . . . . . . . . . 17 (𝑓 = (𝐹𝑦) → ((𝐹𝑥)𝐼𝑓) = ((𝐹𝑥)𝐼(𝐹𝑦)))
154153eleq2d 2823 . . . . . . . . . . . . . . . 16 (𝑓 = (𝐹𝑦) → (𝑐 ∈ ((𝐹𝑥)𝐼𝑓) ↔ 𝑐 ∈ ((𝐹𝑥)𝐼(𝐹𝑦))))
155152, 154rspc2va 3591 . . . . . . . . . . . . . . 15 ((((𝐹𝑥) ∈ (𝐹𝑠) ∧ (𝐹𝑦) ∈ (𝐹𝑡)) ∧ ∀𝑒 ∈ (𝐹𝑠)∀𝑓 ∈ (𝐹𝑡)𝑐 ∈ (𝑒𝐼𝑓)) → 𝑐 ∈ ((𝐹𝑥)𝐼(𝐹𝑦)))
156143, 149, 150, 155syl21anc 836 . . . . . . . . . . . . . 14 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ 𝑐𝑃) ∧ ∀𝑒 ∈ (𝐹𝑠)∀𝑓 ∈ (𝐹𝑡)𝑐 ∈ (𝑒𝐼𝑓)) ∧ (𝑥𝑠𝑦𝑡)) → 𝑐 ∈ ((𝐹𝑥)𝐼(𝐹𝑦)))
157134, 156eqeltrd 2838 . . . . . . . . . . . . 13 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ 𝑐𝑃) ∧ ∀𝑒 ∈ (𝐹𝑠)∀𝑓 ∈ (𝐹𝑡)𝑐 ∈ (𝑒𝐼𝑓)) ∧ (𝑥𝑠𝑦𝑡)) → (𝐹‘(𝐹𝑐)) ∈ ((𝐹𝑥)𝐼(𝐹𝑦)))
1588ad4antr 730 . . . . . . . . . . . . . . 15 (((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ 𝑐𝑃) ∧ (𝑥𝑠𝑦𝑡)) → 𝐹:𝐵1-1-onto𝑃)
159 simp-5l 783 . . . . . . . . . . . . . . . 16 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ 𝑐𝑃) ∧ (𝑥𝑠𝑦𝑡)) ∧ (𝑒𝐵𝑓𝐵)) → 𝜑)
160159, 21sylancom 588 . . . . . . . . . . . . . . 15 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ 𝑐𝑃) ∧ (𝑥𝑠𝑦𝑡)) ∧ (𝑒𝐵𝑓𝐵)) → (𝑒𝐸𝑓) = ((𝐹𝑒)𝐷(𝐹𝑓)))
161 simp-5l 783 . . . . . . . . . . . . . . . 16 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ 𝑐𝑃) ∧ (𝑥𝑠𝑦𝑡)) ∧ (𝑒𝐵𝑓𝐵𝑔𝐵)) → 𝜑)
162161, 23sylancom 588 . . . . . . . . . . . . . . 15 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ 𝑐𝑃) ∧ (𝑥𝑠𝑦𝑡)) ∧ (𝑒𝐵𝑓𝐵𝑔𝐵)) → (𝑔 ∈ (𝑒𝐽𝑓) ↔ (𝐹𝑔) ∈ ((𝐹𝑒)𝐼(𝐹𝑓))))
163 simprl 769 . . . . . . . . . . . . . . . 16 (((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ 𝑐𝑃) ∧ (𝑥𝑠𝑦𝑡)) → 𝑥𝑠)
164139, 163sseldd 3945 . . . . . . . . . . . . . . 15 (((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ 𝑐𝑃) ∧ (𝑥𝑠𝑦𝑡)) → 𝑥𝐵)
165 simprr 771 . . . . . . . . . . . . . . . 16 (((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ 𝑐𝑃) ∧ (𝑥𝑠𝑦𝑡)) → 𝑦𝑡)
166145, 165sseldd 3945 . . . . . . . . . . . . . . 15 (((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ 𝑐𝑃) ∧ (𝑥𝑠𝑦𝑡)) → 𝑦𝐵)
16776ad4antr 730 . . . . . . . . . . . . . . . 16 (((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ 𝑐𝑃) ∧ (𝑥𝑠𝑦𝑡)) → 𝐹:𝑃𝐵)
168 simplr 767 . . . . . . . . . . . . . . . 16 (((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ 𝑐𝑃) ∧ (𝑥𝑠𝑦𝑡)) → 𝑐𝑃)
169167, 168ffvelcdmd 7036 . . . . . . . . . . . . . . 15 (((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ 𝑐𝑃) ∧ (𝑥𝑠𝑦𝑡)) → (𝐹𝑐) ∈ 𝐵)
1703, 4, 5, 17, 18, 19, 158, 160, 162, 164, 166, 169f1otrgitv 27812 . . . . . . . . . . . . . 14 (((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ 𝑐𝑃) ∧ (𝑥𝑠𝑦𝑡)) → ((𝐹𝑐) ∈ (𝑥𝐽𝑦) ↔ (𝐹‘(𝐹𝑐)) ∈ ((𝐹𝑥)𝐼(𝐹𝑦))))
171170adantlr 713 . . . . . . . . . . . . 13 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ 𝑐𝑃) ∧ ∀𝑒 ∈ (𝐹𝑠)∀𝑓 ∈ (𝐹𝑡)𝑐 ∈ (𝑒𝐼𝑓)) ∧ (𝑥𝑠𝑦𝑡)) → ((𝐹𝑐) ∈ (𝑥𝐽𝑦) ↔ (𝐹‘(𝐹𝑐)) ∈ ((𝐹𝑥)𝐼(𝐹𝑦))))
172157, 171mpbird 256 . . . . . . . . . . . 12 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ 𝑐𝑃) ∧ ∀𝑒 ∈ (𝐹𝑠)∀𝑓 ∈ (𝐹𝑡)𝑐 ∈ (𝑒𝐼𝑓)) ∧ (𝑥𝑠𝑦𝑡)) → (𝐹𝑐) ∈ (𝑥𝐽𝑦))
173172ralrimivva 3197 . . . . . . . . . . 11 (((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ 𝑐𝑃) ∧ ∀𝑒 ∈ (𝐹𝑠)∀𝑓 ∈ (𝐹𝑡)𝑐 ∈ (𝑒𝐼𝑓)) → ∀𝑥𝑠𝑦𝑡 (𝐹𝑐) ∈ (𝑥𝐽𝑦))
174173adantllr 717 . . . . . . . . . 10 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑐𝑃) ∧ ∀𝑒 ∈ (𝐹𝑠)∀𝑓 ∈ (𝐹𝑡)𝑐 ∈ (𝑒𝐼𝑓)) → ∀𝑥𝑠𝑦𝑡 (𝐹𝑐) ∈ (𝑥𝐽𝑦))
17576ad4antr 730 . . . . . . . . . . . . 13 (((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑐𝑃) → 𝐹:𝑃𝐵)
176 simpr 485 . . . . . . . . . . . . 13 (((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑐𝑃) → 𝑐𝑃)
177175, 176ffvelcdmd 7036 . . . . . . . . . . . 12 (((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑐𝑃) → (𝐹𝑐) ∈ 𝐵)
178 eleq1 2825 . . . . . . . . . . . . . 14 (𝑏 = (𝐹𝑐) → (𝑏 ∈ (𝑥𝐽𝑦) ↔ (𝐹𝑐) ∈ (𝑥𝐽𝑦)))
1791782ralbidv 3212 . . . . . . . . . . . . 13 (𝑏 = (𝐹𝑐) → (∀𝑥𝑠𝑦𝑡 𝑏 ∈ (𝑥𝐽𝑦) ↔ ∀𝑥𝑠𝑦𝑡 (𝐹𝑐) ∈ (𝑥𝐽𝑦)))
180179adantl 482 . . . . . . . . . . . 12 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑐𝑃) ∧ 𝑏 = (𝐹𝑐)) → (∀𝑥𝑠𝑦𝑡 𝑏 ∈ (𝑥𝐽𝑦) ↔ ∀𝑥𝑠𝑦𝑡 (𝐹𝑐) ∈ (𝑥𝐽𝑦)))
181177, 180rspcedv 3574 . . . . . . . . . . 11 (((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑐𝑃) → (∀𝑥𝑠𝑦𝑡 (𝐹𝑐) ∈ (𝑥𝐽𝑦) → ∃𝑏𝐵𝑥𝑠𝑦𝑡 𝑏 ∈ (𝑥𝐽𝑦)))
182181adantr 481 . . . . . . . . . 10 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑐𝑃) ∧ ∀𝑒 ∈ (𝐹𝑠)∀𝑓 ∈ (𝐹𝑡)𝑐 ∈ (𝑒𝐼𝑓)) → (∀𝑥𝑠𝑦𝑡 (𝐹𝑐) ∈ (𝑥𝐽𝑦) → ∃𝑏𝐵𝑥𝑠𝑦𝑡 𝑏 ∈ (𝑥𝐽𝑦)))
183174, 182mpd 15 . . . . . . . . 9 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑐𝑃) ∧ ∀𝑒 ∈ (𝐹𝑠)∀𝑓 ∈ (𝐹𝑡)𝑐 ∈ (𝑒𝐼𝑓)) → ∃𝑏𝐵𝑥𝑠𝑦𝑡 𝑏 ∈ (𝑥𝐽𝑦))
1846ad3antrrr 728 . . . . . . . . . 10 ((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) → 𝐺 ∈ TarskiG)
185 imassrn 6024 . . . . . . . . . . 11 (𝐹𝑠) ⊆ ran 𝐹
186 f1ofo 6791 . . . . . . . . . . . . 13 (𝐹:𝐵1-1-onto𝑃𝐹:𝐵onto𝑃)
187 forn 6759 . . . . . . . . . . . . 13 (𝐹:𝐵onto𝑃 → ran 𝐹 = 𝑃)
1888, 186, 1873syl 18 . . . . . . . . . . . 12 (𝜑 → ran 𝐹 = 𝑃)
189188ad3antrrr 728 . . . . . . . . . . 11 ((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) → ran 𝐹 = 𝑃)
190185, 189sseqtrid 3996 . . . . . . . . . 10 ((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) → (𝐹𝑠) ⊆ 𝑃)
191 imassrn 6024 . . . . . . . . . . 11 (𝐹𝑡) ⊆ ran 𝐹
192191, 189sseqtrid 3996 . . . . . . . . . 10 ((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) → (𝐹𝑡) ⊆ 𝑃)
19310ad3antrrr 728 . . . . . . . . . . 11 ((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) → 𝐹:𝐵𝑃)
194 simplr 767 . . . . . . . . . . 11 ((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) → 𝑎𝐵)
195193, 194ffvelcdmd 7036 . . . . . . . . . 10 ((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) → (𝐹𝑎) ∈ 𝑃)
1968ad5antr 732 . . . . . . . . . . . . . . . . 17 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹𝑠)) ∧ 𝑣 ∈ (𝐹𝑡)) → 𝐹:𝐵1-1-onto𝑃)
197 ffn 6668 . . . . . . . . . . . . . . . . 17 (𝐹:𝑃𝐵𝐹 Fn 𝑃)
198196, 74, 75, 1974syl 19 . . . . . . . . . . . . . . . 16 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹𝑠)) ∧ 𝑣 ∈ (𝐹𝑡)) → 𝐹 Fn 𝑃)
199190ad2antrr 724 . . . . . . . . . . . . . . . 16 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹𝑠)) ∧ 𝑣 ∈ (𝐹𝑡)) → (𝐹𝑠) ⊆ 𝑃)
200 simplr 767 . . . . . . . . . . . . . . . 16 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹𝑠)) ∧ 𝑣 ∈ (𝐹𝑡)) → 𝑢 ∈ (𝐹𝑠))
201 fnfvima 7183 . . . . . . . . . . . . . . . 16 ((𝐹 Fn 𝑃 ∧ (𝐹𝑠) ⊆ 𝑃𝑢 ∈ (𝐹𝑠)) → (𝐹𝑢) ∈ (𝐹 “ (𝐹𝑠)))
202198, 199, 200, 201syl3anc 1371 . . . . . . . . . . . . . . 15 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹𝑠)) ∧ 𝑣 ∈ (𝐹𝑡)) → (𝐹𝑢) ∈ (𝐹 “ (𝐹𝑠)))
203196, 29syl 17 . . . . . . . . . . . . . . . 16 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹𝑠)) ∧ 𝑣 ∈ (𝐹𝑡)) → 𝐹:𝐵1-1𝑃)
204 simp-5r 784 . . . . . . . . . . . . . . . . . 18 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹𝑠)) ∧ 𝑣 ∈ (𝐹𝑡)) → (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵))
205204simpld 495 . . . . . . . . . . . . . . . . 17 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹𝑠)) ∧ 𝑣 ∈ (𝐹𝑡)) → 𝑠 ∈ 𝒫 𝐵)
206205elpwid 4569 . . . . . . . . . . . . . . . 16 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹𝑠)) ∧ 𝑣 ∈ (𝐹𝑡)) → 𝑠𝐵)
207 f1imacnv 6800 . . . . . . . . . . . . . . . 16 ((𝐹:𝐵1-1𝑃𝑠𝐵) → (𝐹 “ (𝐹𝑠)) = 𝑠)
208203, 206, 207syl2anc 584 . . . . . . . . . . . . . . 15 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹𝑠)) ∧ 𝑣 ∈ (𝐹𝑡)) → (𝐹 “ (𝐹𝑠)) = 𝑠)
209202, 208eleqtrd 2840 . . . . . . . . . . . . . 14 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹𝑠)) ∧ 𝑣 ∈ (𝐹𝑡)) → (𝐹𝑢) ∈ 𝑠)
210192ad2antrr 724 . . . . . . . . . . . . . . . 16 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹𝑠)) ∧ 𝑣 ∈ (𝐹𝑡)) → (𝐹𝑡) ⊆ 𝑃)
211 simpr 485 . . . . . . . . . . . . . . . 16 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹𝑠)) ∧ 𝑣 ∈ (𝐹𝑡)) → 𝑣 ∈ (𝐹𝑡))
212 fnfvima 7183 . . . . . . . . . . . . . . . 16 ((𝐹 Fn 𝑃 ∧ (𝐹𝑡) ⊆ 𝑃𝑣 ∈ (𝐹𝑡)) → (𝐹𝑣) ∈ (𝐹 “ (𝐹𝑡)))
213198, 210, 211, 212syl3anc 1371 . . . . . . . . . . . . . . 15 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹𝑠)) ∧ 𝑣 ∈ (𝐹𝑡)) → (𝐹𝑣) ∈ (𝐹 “ (𝐹𝑡)))
214204simprd 496 . . . . . . . . . . . . . . . . 17 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹𝑠)) ∧ 𝑣 ∈ (𝐹𝑡)) → 𝑡 ∈ 𝒫 𝐵)
215214elpwid 4569 . . . . . . . . . . . . . . . 16 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹𝑠)) ∧ 𝑣 ∈ (𝐹𝑡)) → 𝑡𝐵)
216 f1imacnv 6800 . . . . . . . . . . . . . . . 16 ((𝐹:𝐵1-1𝑃𝑡𝐵) → (𝐹 “ (𝐹𝑡)) = 𝑡)
217203, 215, 216syl2anc 584 . . . . . . . . . . . . . . 15 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹𝑠)) ∧ 𝑣 ∈ (𝐹𝑡)) → (𝐹 “ (𝐹𝑡)) = 𝑡)
218213, 217eleqtrd 2840 . . . . . . . . . . . . . 14 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹𝑠)) ∧ 𝑣 ∈ (𝐹𝑡)) → (𝐹𝑣) ∈ 𝑡)
219 simpllr 774 . . . . . . . . . . . . . 14 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹𝑠)) ∧ 𝑣 ∈ (𝐹𝑡)) → ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦))
220 eleq1 2825 . . . . . . . . . . . . . . 15 (𝑥 = (𝐹𝑢) → (𝑥 ∈ (𝑎𝐽𝑦) ↔ (𝐹𝑢) ∈ (𝑎𝐽𝑦)))
221 oveq2 7365 . . . . . . . . . . . . . . . 16 (𝑦 = (𝐹𝑣) → (𝑎𝐽𝑦) = (𝑎𝐽(𝐹𝑣)))
222221eleq2d 2823 . . . . . . . . . . . . . . 15 (𝑦 = (𝐹𝑣) → ((𝐹𝑢) ∈ (𝑎𝐽𝑦) ↔ (𝐹𝑢) ∈ (𝑎𝐽(𝐹𝑣))))
223220, 222rspc2va 3591 . . . . . . . . . . . . . 14 ((((𝐹𝑢) ∈ 𝑠 ∧ (𝐹𝑣) ∈ 𝑡) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) → (𝐹𝑢) ∈ (𝑎𝐽(𝐹𝑣)))
224209, 218, 219, 223syl21anc 836 . . . . . . . . . . . . 13 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹𝑠)) ∧ 𝑣 ∈ (𝐹𝑡)) → (𝐹𝑢) ∈ (𝑎𝐽(𝐹𝑣)))
225 simp-6l 785 . . . . . . . . . . . . . . 15 (((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹𝑠)) ∧ 𝑣 ∈ (𝐹𝑡)) ∧ (𝑒𝐵𝑓𝐵)) → 𝜑)
226225, 21sylancom 588 . . . . . . . . . . . . . 14 (((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹𝑠)) ∧ 𝑣 ∈ (𝐹𝑡)) ∧ (𝑒𝐵𝑓𝐵)) → (𝑒𝐸𝑓) = ((𝐹𝑒)𝐷(𝐹𝑓)))
227 simp-6l 785 . . . . . . . . . . . . . . 15 (((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹𝑠)) ∧ 𝑣 ∈ (𝐹𝑡)) ∧ (𝑒𝐵𝑓𝐵𝑔𝐵)) → 𝜑)
228227, 23sylancom 588 . . . . . . . . . . . . . 14 (((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹𝑠)) ∧ 𝑣 ∈ (𝐹𝑡)) ∧ (𝑒𝐵𝑓𝐵𝑔𝐵)) → (𝑔 ∈ (𝑒𝐽𝑓) ↔ (𝐹𝑔) ∈ ((𝐹𝑒)𝐼(𝐹𝑓))))
229 simp-4r 782 . . . . . . . . . . . . . 14 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹𝑠)) ∧ 𝑣 ∈ (𝐹𝑡)) → 𝑎𝐵)
230210, 211sseldd 3945 . . . . . . . . . . . . . . 15 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹𝑠)) ∧ 𝑣 ∈ (𝐹𝑡)) → 𝑣𝑃)
231 f1ocnvdm 7231 . . . . . . . . . . . . . . 15 ((𝐹:𝐵1-1-onto𝑃𝑣𝑃) → (𝐹𝑣) ∈ 𝐵)
232196, 230, 231syl2anc 584 . . . . . . . . . . . . . 14 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹𝑠)) ∧ 𝑣 ∈ (𝐹𝑡)) → (𝐹𝑣) ∈ 𝐵)
233199, 200sseldd 3945 . . . . . . . . . . . . . . 15 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹𝑠)) ∧ 𝑣 ∈ (𝐹𝑡)) → 𝑢𝑃)
234 f1ocnvdm 7231 . . . . . . . . . . . . . . 15 ((𝐹:𝐵1-1-onto𝑃𝑢𝑃) → (𝐹𝑢) ∈ 𝐵)
235196, 233, 234syl2anc 584 . . . . . . . . . . . . . 14 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹𝑠)) ∧ 𝑣 ∈ (𝐹𝑡)) → (𝐹𝑢) ∈ 𝐵)
2363, 4, 5, 17, 18, 19, 196, 226, 228, 229, 232, 235f1otrgitv 27812 . . . . . . . . . . . . 13 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹𝑠)) ∧ 𝑣 ∈ (𝐹𝑡)) → ((𝐹𝑢) ∈ (𝑎𝐽(𝐹𝑣)) ↔ (𝐹‘(𝐹𝑢)) ∈ ((𝐹𝑎)𝐼(𝐹‘(𝐹𝑣)))))
237224, 236mpbid 231 . . . . . . . . . . . 12 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹𝑠)) ∧ 𝑣 ∈ (𝐹𝑡)) → (𝐹‘(𝐹𝑢)) ∈ ((𝐹𝑎)𝐼(𝐹‘(𝐹𝑣))))
238 f1ocnvfv2 7223 . . . . . . . . . . . . 13 ((𝐹:𝐵1-1-onto𝑃𝑢𝑃) → (𝐹‘(𝐹𝑢)) = 𝑢)
239196, 233, 238syl2anc 584 . . . . . . . . . . . 12 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹𝑠)) ∧ 𝑣 ∈ (𝐹𝑡)) → (𝐹‘(𝐹𝑢)) = 𝑢)
240 f1ocnvfv2 7223 . . . . . . . . . . . . . 14 ((𝐹:𝐵1-1-onto𝑃𝑣𝑃) → (𝐹‘(𝐹𝑣)) = 𝑣)
241196, 230, 240syl2anc 584 . . . . . . . . . . . . 13 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹𝑠)) ∧ 𝑣 ∈ (𝐹𝑡)) → (𝐹‘(𝐹𝑣)) = 𝑣)
242241oveq2d 7373 . . . . . . . . . . . 12 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹𝑠)) ∧ 𝑣 ∈ (𝐹𝑡)) → ((𝐹𝑎)𝐼(𝐹‘(𝐹𝑣))) = ((𝐹𝑎)𝐼𝑣))
243237, 239, 2423eltr3d 2852 . . . . . . . . . . 11 ((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹𝑠)) ∧ 𝑣 ∈ (𝐹𝑡)) → 𝑢 ∈ ((𝐹𝑎)𝐼𝑣))
2442433impa 1110 . . . . . . . . . 10 (((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹𝑠) ∧ 𝑣 ∈ (𝐹𝑡)) → 𝑢 ∈ ((𝐹𝑎)𝐼𝑣))
2453, 4, 5, 184, 190, 192, 195, 244axtgcont 27411 . . . . . . . . 9 ((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) → ∃𝑐𝑃𝑒 ∈ (𝐹𝑠)∀𝑓 ∈ (𝐹𝑡)𝑐 ∈ (𝑒𝐼𝑓))
246183, 245r19.29a 3159 . . . . . . . 8 ((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎𝐵) ∧ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦)) → ∃𝑏𝐵𝑥𝑠𝑦𝑡 𝑏 ∈ (𝑥𝐽𝑦))
247246rexlimdva2 3154 . . . . . . 7 ((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) → (∃𝑎𝐵𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦) → ∃𝑏𝐵𝑥𝑠𝑦𝑡 𝑏 ∈ (𝑥𝐽𝑦)))
248247ralrimivva 3197 . . . . . 6 (𝜑 → ∀𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵(∃𝑎𝐵𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦) → ∃𝑏𝐵𝑥𝑠𝑦𝑡 𝑏 ∈ (𝑥𝐽𝑦)))
24973, 131, 2483jca 1128 . . . . 5 (𝜑 → (∀𝑥𝐵𝑦𝐵 (𝑦 ∈ (𝑥𝐽𝑥) → 𝑥 = 𝑦) ∧ ∀𝑥𝐵𝑦𝐵𝑧𝐵𝑢𝐵𝑣𝐵 ((𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧)) → ∃𝑎𝐵 (𝑎 ∈ (𝑢𝐽𝑦) ∧ 𝑎 ∈ (𝑣𝐽𝑥))) ∧ ∀𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵(∃𝑎𝐵𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦) → ∃𝑏𝐵𝑥𝑠𝑦𝑡 𝑏 ∈ (𝑥𝐽𝑦))))
25017, 18, 19istrkgb 27397 . . . . 5 (𝐻 ∈ TarskiGB ↔ (𝐻 ∈ V ∧ (∀𝑥𝐵𝑦𝐵 (𝑦 ∈ (𝑥𝐽𝑥) → 𝑥 = 𝑦) ∧ ∀𝑥𝐵𝑦𝐵𝑧𝐵𝑢𝐵𝑣𝐵 ((𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧)) → ∃𝑎𝐵 (𝑎 ∈ (𝑢𝐽𝑦) ∧ 𝑎 ∈ (𝑣𝐽𝑥))) ∧ ∀𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵(∃𝑎𝐵𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐽𝑦) → ∃𝑏𝐵𝑥𝑠𝑦𝑡 𝑏 ∈ (𝑥𝐽𝑦)))))
2512, 249, 250sylanbrc 583 . . . 4 (𝜑𝐻 ∈ TarskiGB)
25256, 251elind 4154 . . 3 (𝜑𝐻 ∈ (TarskiGC ∩ TarskiGB))
2536ad9antr 740 . . . . . . . . . . . . . . . . 17 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → 𝐺 ∈ TarskiG)
25410ad9antr 740 . . . . . . . . . . . . . . . . . 18 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → 𝐹:𝐵𝑃)
255 simp-9r 792 . . . . . . . . . . . . . . . . . 18 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → 𝑥𝐵)
256254, 255ffvelcdmd 7036 . . . . . . . . . . . . . . . . 17 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → (𝐹𝑥) ∈ 𝑃)
257 simp-8r 790 . . . . . . . . . . . . . . . . . 18 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → 𝑦𝐵)
258254, 257ffvelcdmd 7036 . . . . . . . . . . . . . . . . 17 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → (𝐹𝑦) ∈ 𝑃)
259 simp-7r 788 . . . . . . . . . . . . . . . . . 18 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → 𝑧𝐵)
260254, 259ffvelcdmd 7036 . . . . . . . . . . . . . . . . 17 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → (𝐹𝑧) ∈ 𝑃)
261 simp-5r 784 . . . . . . . . . . . . . . . . . 18 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → 𝑎𝐵)
262254, 261ffvelcdmd 7036 . . . . . . . . . . . . . . . . 17 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → (𝐹𝑎) ∈ 𝑃)
263 simp-4r 782 . . . . . . . . . . . . . . . . . 18 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → 𝑏𝐵)
264254, 263ffvelcdmd 7036 . . . . . . . . . . . . . . . . 17 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → (𝐹𝑏) ∈ 𝑃)
265 simpllr 774 . . . . . . . . . . . . . . . . . 18 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → 𝑐𝐵)
266254, 265ffvelcdmd 7036 . . . . . . . . . . . . . . . . 17 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → (𝐹𝑐) ∈ 𝑃)
267 simp-6r 786 . . . . . . . . . . . . . . . . . 18 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → 𝑢𝐵)
268254, 267ffvelcdmd 7036 . . . . . . . . . . . . . . . . 17 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → (𝐹𝑢) ∈ 𝑃)
269 simplr 767 . . . . . . . . . . . . . . . . . 18 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → 𝑣𝐵)
270254, 269ffvelcdmd 7036 . . . . . . . . . . . . . . . . 17 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → (𝐹𝑣) ∈ 𝑃)
2718ad9antr 740 . . . . . . . . . . . . . . . . . . 19 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → 𝐹:𝐵1-1-onto𝑃)
272271, 255jca 512 . . . . . . . . . . . . . . . . . 18 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → (𝐹:𝐵1-1-onto𝑃𝑥𝐵))
273 simprl1 1218 . . . . . . . . . . . . . . . . . 18 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → 𝑥𝑦)
274 dff1o6 7221 . . . . . . . . . . . . . . . . . . . . . . 23 (𝐹:𝐵1-1-onto𝑃 ↔ (𝐹 Fn 𝐵 ∧ ran 𝐹 = 𝑃 ∧ ∀𝑥𝐵𝑦𝐵 ((𝐹𝑥) = (𝐹𝑦) → 𝑥 = 𝑦)))
275274simp3bi 1147 . . . . . . . . . . . . . . . . . . . . . 22 (𝐹:𝐵1-1-onto𝑃 → ∀𝑥𝐵𝑦𝐵 ((𝐹𝑥) = (𝐹𝑦) → 𝑥 = 𝑦))
276275r19.21bi 3234 . . . . . . . . . . . . . . . . . . . . 21 ((𝐹:𝐵1-1-onto𝑃𝑥𝐵) → ∀𝑦𝐵 ((𝐹𝑥) = (𝐹𝑦) → 𝑥 = 𝑦))
277276r19.21bi 3234 . . . . . . . . . . . . . . . . . . . 20 (((𝐹:𝐵1-1-onto𝑃𝑥𝐵) ∧ 𝑦𝐵) → ((𝐹𝑥) = (𝐹𝑦) → 𝑥 = 𝑦))
278277necon3d 2964 . . . . . . . . . . . . . . . . . . 19 (((𝐹:𝐵1-1-onto𝑃𝑥𝐵) ∧ 𝑦𝐵) → (𝑥𝑦 → (𝐹𝑥) ≠ (𝐹𝑦)))
279278imp 407 . . . . . . . . . . . . . . . . . 18 ((((𝐹:𝐵1-1-onto𝑃𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑥𝑦) → (𝐹𝑥) ≠ (𝐹𝑦))
280272, 257, 273, 279syl21anc 836 . . . . . . . . . . . . . . . . 17 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → (𝐹𝑥) ≠ (𝐹𝑦))
281 simprl2 1219 . . . . . . . . . . . . . . . . . 18 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → 𝑦 ∈ (𝑥𝐽𝑧))
28221ex 413 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → ((𝑒𝐵𝑓𝐵) → (𝑒𝐸𝑓) = ((𝐹𝑒)𝐷(𝐹𝑓))))
283282ad9antr 740 . . . . . . . . . . . . . . . . . . . 20 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → ((𝑒𝐵𝑓𝐵) → (𝑒𝐸𝑓) = ((𝐹𝑒)𝐷(𝐹𝑓))))
284283imp 407 . . . . . . . . . . . . . . . . . . 19 (((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) ∧ (𝑒𝐵𝑓𝐵)) → (𝑒𝐸𝑓) = ((𝐹𝑒)𝐷(𝐹𝑓)))
28523ex 413 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → ((𝑒𝐵𝑓𝐵𝑔𝐵) → (𝑔 ∈ (𝑒𝐽𝑓) ↔ (𝐹𝑔) ∈ ((𝐹𝑒)𝐼(𝐹𝑓)))))
286285ad9antr 740 . . . . . . . . . . . . . . . . . . . 20 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → ((𝑒𝐵𝑓𝐵𝑔𝐵) → (𝑔 ∈ (𝑒𝐽𝑓) ↔ (𝐹𝑔) ∈ ((𝐹𝑒)𝐼(𝐹𝑓)))))
287286imp 407 . . . . . . . . . . . . . . . . . . 19 (((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) ∧ (𝑒𝐵𝑓𝐵𝑔𝐵)) → (𝑔 ∈ (𝑒𝐽𝑓) ↔ (𝐹𝑔) ∈ ((𝐹𝑒)𝐼(𝐹𝑓))))
2883, 4, 5, 17, 18, 19, 271, 284, 287, 255, 259, 257f1otrgitv 27812 . . . . . . . . . . . . . . . . . 18 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → (𝑦 ∈ (𝑥𝐽𝑧) ↔ (𝐹𝑦) ∈ ((𝐹𝑥)𝐼(𝐹𝑧))))
289281, 288mpbid 231 . . . . . . . . . . . . . . . . 17 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → (𝐹𝑦) ∈ ((𝐹𝑥)𝐼(𝐹𝑧)))
290 simprl3 1220 . . . . . . . . . . . . . . . . . 18 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → 𝑏 ∈ (𝑎𝐽𝑐))
2913, 4, 5, 17, 18, 19, 271, 284, 287, 261, 265, 263f1otrgitv 27812 . . . . . . . . . . . . . . . . . 18 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → (𝑏 ∈ (𝑎𝐽𝑐) ↔ (𝐹𝑏) ∈ ((𝐹𝑎)𝐼(𝐹𝑐))))
292290, 291mpbid 231 . . . . . . . . . . . . . . . . 17 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → (𝐹𝑏) ∈ ((𝐹𝑎)𝐼(𝐹𝑐)))
293 simprr 771 . . . . . . . . . . . . . . . . . . . 20 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))
294293simpld 495 . . . . . . . . . . . . . . . . . . 19 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → ((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)))
295294simpld 495 . . . . . . . . . . . . . . . . . 18 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → (𝑥𝐸𝑦) = (𝑎𝐸𝑏))
2963, 4, 5, 17, 18, 19, 271, 284, 287, 255, 257f1otrgds 27811 . . . . . . . . . . . . . . . . . 18 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → (𝑥𝐸𝑦) = ((𝐹𝑥)𝐷(𝐹𝑦)))
2973, 4, 5, 17, 18, 19, 271, 284, 287, 261, 263f1otrgds 27811 . . . . . . . . . . . . . . . . . 18 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → (𝑎𝐸𝑏) = ((𝐹𝑎)𝐷(𝐹𝑏)))
298295, 296, 2973eqtr3d 2784 . . . . . . . . . . . . . . . . 17 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → ((𝐹𝑥)𝐷(𝐹𝑦)) = ((𝐹𝑎)𝐷(𝐹𝑏)))
299294simprd 496 . . . . . . . . . . . . . . . . . 18 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → (𝑦𝐸𝑧) = (𝑏𝐸𝑐))
3003, 4, 5, 17, 18, 19, 271, 284, 287, 257, 259f1otrgds 27811 . . . . . . . . . . . . . . . . . 18 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → (𝑦𝐸𝑧) = ((𝐹𝑦)𝐷(𝐹𝑧)))
3013, 4, 5, 17, 18, 19, 271, 284, 287, 263, 265f1otrgds 27811 . . . . . . . . . . . . . . . . . 18 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → (𝑏𝐸𝑐) = ((𝐹𝑏)𝐷(𝐹𝑐)))
302299, 300, 3013eqtr3d 2784 . . . . . . . . . . . . . . . . 17 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → ((𝐹𝑦)𝐷(𝐹𝑧)) = ((𝐹𝑏)𝐷(𝐹𝑐)))
303293simprd 496 . . . . . . . . . . . . . . . . . . 19 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣)))
304303simpld 495 . . . . . . . . . . . . . . . . . 18 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → (𝑥𝐸𝑢) = (𝑎𝐸𝑣))
3053, 4, 5, 17, 18, 19, 271, 284, 287, 255, 267f1otrgds 27811 . . . . . . . . . . . . . . . . . 18 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → (𝑥𝐸𝑢) = ((𝐹𝑥)𝐷(𝐹𝑢)))
3063, 4, 5, 17, 18, 19, 271, 284, 287, 261, 269f1otrgds 27811 . . . . . . . . . . . . . . . . . 18 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → (𝑎𝐸𝑣) = ((𝐹𝑎)𝐷(𝐹𝑣)))
307304, 305, 3063eqtr3d 2784 . . . . . . . . . . . . . . . . 17 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → ((𝐹𝑥)𝐷(𝐹𝑢)) = ((𝐹𝑎)𝐷(𝐹𝑣)))
308303simprd 496 . . . . . . . . . . . . . . . . . 18 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → (𝑦𝐸𝑢) = (𝑏𝐸𝑣))
3093, 4, 5, 17, 18, 19, 271, 284, 287, 257, 267f1otrgds 27811 . . . . . . . . . . . . . . . . . 18 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → (𝑦𝐸𝑢) = ((𝐹𝑦)𝐷(𝐹𝑢)))
3103, 4, 5, 17, 18, 19, 271, 284, 287, 263, 269f1otrgds 27811 . . . . . . . . . . . . . . . . . 18 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → (𝑏𝐸𝑣) = ((𝐹𝑏)𝐷(𝐹𝑣)))
311308, 309, 3103eqtr3d 2784 . . . . . . . . . . . . . . . . 17 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → ((𝐹𝑦)𝐷(𝐹𝑢)) = ((𝐹𝑏)𝐷(𝐹𝑣)))
3123, 4, 5, 253, 256, 258, 260, 262, 264, 266, 268, 270, 280, 289, 292, 298, 302, 307, 311axtg5seg 27407 . . . . . . . . . . . . . . . 16 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → ((𝐹𝑧)𝐷(𝐹𝑢)) = ((𝐹𝑐)𝐷(𝐹𝑣)))
3133, 4, 5, 17, 18, 19, 271, 284, 287, 259, 267f1otrgds 27811 . . . . . . . . . . . . . . . 16 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → (𝑧𝐸𝑢) = ((𝐹𝑧)𝐷(𝐹𝑢)))
3143, 4, 5, 17, 18, 19, 271, 284, 287, 265, 269f1otrgds 27811 . . . . . . . . . . . . . . . 16 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → (𝑐𝐸𝑣) = ((𝐹𝑐)𝐷(𝐹𝑣)))
315312, 313, 3143eqtr4d 2786 . . . . . . . . . . . . . . 15 ((((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) ∧ ((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → (𝑧𝐸𝑢) = (𝑐𝐸𝑣))
316315ex 413 . . . . . . . . . . . . . 14 (((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) ∧ 𝑣𝐵) → (((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣)))) → (𝑧𝐸𝑢) = (𝑐𝐸𝑣)))
317316ralrimiva 3143 . . . . . . . . . . . . 13 ((((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) ∧ 𝑐𝐵) → ∀𝑣𝐵 (((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣)))) → (𝑧𝐸𝑢) = (𝑐𝐸𝑣)))
318317ralrimiva 3143 . . . . . . . . . . . 12 (((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) ∧ 𝑏𝐵) → ∀𝑐𝐵𝑣𝐵 (((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣)))) → (𝑧𝐸𝑢) = (𝑐𝐸𝑣)))
319318ralrimiva 3143 . . . . . . . . . . 11 ((((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) ∧ 𝑎𝐵) → ∀𝑏𝐵𝑐𝐵𝑣𝐵 (((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣)))) → (𝑧𝐸𝑢) = (𝑐𝐸𝑣)))
320319ralrimiva 3143 . . . . . . . . . 10 (((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) ∧ 𝑢𝐵) → ∀𝑎𝐵𝑏𝐵𝑐𝐵𝑣𝐵 (((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣)))) → (𝑧𝐸𝑢) = (𝑐𝐸𝑣)))
321320ralrimiva 3143 . . . . . . . . 9 ((((𝜑𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑧𝐵) → ∀𝑢𝐵𝑎𝐵𝑏𝐵𝑐𝐵𝑣𝐵 (((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣)))) → (𝑧𝐸𝑢) = (𝑐𝐸𝑣)))
322321ralrimiva 3143 . . . . . . . 8 (((𝜑𝑥𝐵) ∧ 𝑦𝐵) → ∀𝑧𝐵𝑢𝐵𝑎𝐵𝑏𝐵𝑐𝐵𝑣𝐵 (((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣)))) → (𝑧𝐸𝑢) = (𝑐𝐸𝑣)))
323322ralrimiva 3143 . . . . . . 7 ((𝜑𝑥𝐵) → ∀𝑦𝐵𝑧𝐵𝑢𝐵𝑎𝐵𝑏𝐵𝑐𝐵𝑣𝐵 (((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣)))) → (𝑧𝐸𝑢) = (𝑐𝐸𝑣)))
324323ralrimiva 3143 . . . . . 6 (𝜑 → ∀𝑥𝐵𝑦𝐵𝑧𝐵𝑢𝐵𝑎𝐵𝑏𝐵𝑐𝐵𝑣𝐵 (((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣)))) → (𝑧𝐸𝑢) = (𝑐𝐸𝑣)))
325 simp-4l 781 . . . . . . . . . 10 (((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑎𝐵𝑏𝐵)) ∧ 𝑤𝑃) ∧ ((𝐹𝑦) ∈ ((𝐹𝑥)𝐼𝑤) ∧ ((𝐹𝑦)𝐷𝑤) = ((𝐹𝑎)𝐷(𝐹𝑏)))) → 𝜑)
326 simplr 767 . . . . . . . . . 10 (((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑎𝐵𝑏𝐵)) ∧ 𝑤𝑃) ∧ ((𝐹𝑦) ∈ ((𝐹𝑥)𝐼𝑤) ∧ ((𝐹𝑦)𝐷𝑤) = ((𝐹𝑎)𝐷(𝐹𝑏)))) → 𝑤𝑃)
327 simprl 769 . . . . . . . . . . . 12 (((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑎𝐵𝑏𝐵)) ∧ 𝑤𝑃) ∧ ((𝐹𝑦) ∈ ((𝐹𝑥)𝐼𝑤) ∧ ((𝐹𝑦)𝐷𝑤) = ((𝐹𝑎)𝐷(𝐹𝑏)))) → (𝐹𝑦) ∈ ((𝐹𝑥)𝐼𝑤))
328325, 8syl 17 . . . . . . . . . . . . . 14 (((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑎𝐵𝑏𝐵)) ∧ 𝑤𝑃) ∧ ((𝐹𝑦) ∈ ((𝐹𝑥)𝐼𝑤) ∧ ((𝐹𝑦)𝐷𝑤) = ((𝐹𝑎)𝐷(𝐹𝑏)))) → 𝐹:𝐵1-1-onto𝑃)
329 f1ocnvfv2 7223 . . . . . . . . . . . . . 14 ((𝐹:𝐵1-1-onto𝑃𝑤𝑃) → (𝐹‘(𝐹𝑤)) = 𝑤)
330328, 326, 329syl2anc 584 . . . . . . . . . . . . 13 (((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑎𝐵𝑏𝐵)) ∧ 𝑤𝑃) ∧ ((𝐹𝑦) ∈ ((𝐹𝑥)𝐼𝑤) ∧ ((𝐹𝑦)𝐷𝑤) = ((𝐹𝑎)𝐷(𝐹𝑏)))) → (𝐹‘(𝐹𝑤)) = 𝑤)
331330oveq2d 7373 . . . . . . . . . . . 12 (((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑎𝐵𝑏𝐵)) ∧ 𝑤𝑃) ∧ ((𝐹𝑦) ∈ ((𝐹𝑥)𝐼𝑤) ∧ ((𝐹𝑦)𝐷𝑤) = ((𝐹𝑎)𝐷(𝐹𝑏)))) → ((𝐹𝑥)𝐼(𝐹‘(𝐹𝑤))) = ((𝐹𝑥)𝐼𝑤))
332327, 331eleqtrrd 2841 . . . . . . . . . . 11 (((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑎𝐵𝑏𝐵)) ∧ 𝑤𝑃) ∧ ((𝐹𝑦) ∈ ((𝐹𝑥)𝐼𝑤) ∧ ((𝐹𝑦)𝐷𝑤) = ((𝐹𝑎)𝐷(𝐹𝑏)))) → (𝐹𝑦) ∈ ((𝐹𝑥)𝐼(𝐹‘(𝐹𝑤))))
333325, 21sylan 580 . . . . . . . . . . . 12 ((((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑎𝐵𝑏𝐵)) ∧ 𝑤𝑃) ∧ ((𝐹𝑦) ∈ ((𝐹𝑥)𝐼𝑤) ∧ ((𝐹𝑦)𝐷𝑤) = ((𝐹𝑎)𝐷(𝐹𝑏)))) ∧ (𝑒𝐵𝑓𝐵)) → (𝑒𝐸𝑓) = ((𝐹𝑒)𝐷(𝐹𝑓)))
334325, 23sylan 580 . . . . . . . . . . . 12 ((((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑎𝐵𝑏𝐵)) ∧ 𝑤𝑃) ∧ ((𝐹𝑦) ∈ ((𝐹𝑥)𝐼𝑤) ∧ ((𝐹𝑦)𝐷𝑤) = ((𝐹𝑎)𝐷(𝐹𝑏)))) ∧ (𝑒𝐵𝑓𝐵𝑔𝐵)) → (𝑔 ∈ (𝑒𝐽𝑓) ↔ (𝐹𝑔) ∈ ((𝐹𝑒)𝐼(𝐹𝑓))))
33512ad3antrrr 728 . . . . . . . . . . . 12 (((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑎𝐵𝑏𝐵)) ∧ 𝑤𝑃) ∧ ((𝐹𝑦) ∈ ((𝐹𝑥)𝐼𝑤) ∧ ((𝐹𝑦)𝐷𝑤) = ((𝐹𝑎)𝐷(𝐹𝑏)))) → 𝑥𝐵)
33676ffvelcdmda 7035 . . . . . . . . . . . . 13 ((𝜑𝑤𝑃) → (𝐹𝑤) ∈ 𝐵)
337325, 326, 336syl2anc 584 . . . . . . . . . . . 12 (((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑎𝐵𝑏𝐵)) ∧ 𝑤𝑃) ∧ ((𝐹𝑦) ∈ ((𝐹𝑥)𝐼𝑤) ∧ ((𝐹𝑦)𝐷𝑤) = ((𝐹𝑎)𝐷(𝐹𝑏)))) → (𝐹𝑤) ∈ 𝐵)
33814ad3antrrr 728 . . . . . . . . . . . 12 (((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑎𝐵𝑏𝐵)) ∧ 𝑤𝑃) ∧ ((𝐹𝑦) ∈ ((𝐹𝑥)𝐼𝑤) ∧ ((𝐹𝑦)𝐷𝑤) = ((𝐹𝑎)𝐷(𝐹𝑏)))) → 𝑦𝐵)
3393, 4, 5, 17, 18, 19, 328, 333, 334, 335, 337, 338f1otrgitv 27812 . . . . . . . . . . 11 (((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑎𝐵𝑏𝐵)) ∧ 𝑤𝑃) ∧ ((𝐹𝑦) ∈ ((𝐹𝑥)𝐼𝑤) ∧ ((𝐹𝑦)𝐷𝑤) = ((𝐹𝑎)𝐷(𝐹𝑏)))) → (𝑦 ∈ (𝑥𝐽(𝐹𝑤)) ↔ (𝐹𝑦) ∈ ((𝐹𝑥)𝐼(𝐹‘(𝐹𝑤)))))
340332, 339mpbird 256 . . . . . . . . . 10 (((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑎𝐵𝑏𝐵)) ∧ 𝑤𝑃) ∧ ((𝐹𝑦) ∈ ((𝐹𝑥)𝐼𝑤) ∧ ((𝐹𝑦)𝐷𝑤) = ((𝐹𝑎)𝐷(𝐹𝑏)))) → 𝑦 ∈ (𝑥𝐽(𝐹𝑤)))
3413, 4, 5, 17, 18, 19, 328, 333, 334, 338, 337f1otrgds 27811 . . . . . . . . . . . 12 (((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑎𝐵𝑏𝐵)) ∧ 𝑤𝑃) ∧ ((𝐹𝑦) ∈ ((𝐹𝑥)𝐼𝑤) ∧ ((𝐹𝑦)𝐷𝑤) = ((𝐹𝑎)𝐷(𝐹𝑏)))) → (𝑦𝐸(𝐹𝑤)) = ((𝐹𝑦)𝐷(𝐹‘(𝐹𝑤))))
342330oveq2d 7373 . . . . . . . . . . . 12 (((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑎𝐵𝑏𝐵)) ∧ 𝑤𝑃) ∧ ((𝐹𝑦) ∈ ((𝐹𝑥)𝐼𝑤) ∧ ((𝐹𝑦)𝐷𝑤) = ((𝐹𝑎)𝐷(𝐹𝑏)))) → ((𝐹𝑦)𝐷(𝐹‘(𝐹𝑤))) = ((𝐹𝑦)𝐷𝑤))
343 simprr 771 . . . . . . . . . . . 12 (((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑎𝐵𝑏𝐵)) ∧ 𝑤𝑃) ∧ ((𝐹𝑦) ∈ ((𝐹𝑥)𝐼𝑤) ∧ ((𝐹𝑦)𝐷𝑤) = ((𝐹𝑎)𝐷(𝐹𝑏)))) → ((𝐹𝑦)𝐷𝑤) = ((𝐹𝑎)𝐷(𝐹𝑏)))
344341, 342, 3433eqtrd 2780 . . . . . . . . . . 11 (((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑎𝐵𝑏𝐵)) ∧ 𝑤𝑃) ∧ ((𝐹𝑦) ∈ ((𝐹𝑥)𝐼𝑤) ∧ ((𝐹𝑦)𝐷𝑤) = ((𝐹𝑎)𝐷(𝐹𝑏)))) → (𝑦𝐸(𝐹𝑤)) = ((𝐹𝑎)𝐷(𝐹𝑏)))
345 simprl 769 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑎𝐵𝑏𝐵)) → 𝑎𝐵)
346345ad2antrr 724 . . . . . . . . . . . 12 (((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑎𝐵𝑏𝐵)) ∧ 𝑤𝑃) ∧ ((𝐹𝑦) ∈ ((𝐹𝑥)𝐼𝑤) ∧ ((𝐹𝑦)𝐷𝑤) = ((𝐹𝑎)𝐷(𝐹𝑏)))) → 𝑎𝐵)
347 simprr 771 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑎𝐵𝑏𝐵)) → 𝑏𝐵)
348347ad2antrr 724 . . . . . . . . . . . 12 (((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑎𝐵𝑏𝐵)) ∧ 𝑤𝑃) ∧ ((𝐹𝑦) ∈ ((𝐹𝑥)𝐼𝑤) ∧ ((𝐹𝑦)𝐷𝑤) = ((𝐹𝑎)𝐷(𝐹𝑏)))) → 𝑏𝐵)
3493, 4, 5, 17, 18, 19, 328, 333, 334, 346, 348f1otrgds 27811 . . . . . . . . . . 11 (((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑎𝐵𝑏𝐵)) ∧ 𝑤𝑃) ∧ ((𝐹𝑦) ∈ ((𝐹𝑥)𝐼𝑤) ∧ ((𝐹𝑦)𝐷𝑤) = ((𝐹𝑎)𝐷(𝐹𝑏)))) → (𝑎𝐸𝑏) = ((𝐹𝑎)𝐷(𝐹𝑏)))
350344, 349eqtr4d 2779 . . . . . . . . . 10 (((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑎𝐵𝑏𝐵)) ∧ 𝑤𝑃) ∧ ((𝐹𝑦) ∈ ((𝐹𝑥)𝐼𝑤) ∧ ((𝐹𝑦)𝐷𝑤) = ((𝐹𝑎)𝐷(𝐹𝑏)))) → (𝑦𝐸(𝐹𝑤)) = (𝑎𝐸𝑏))
351 oveq2 7365 . . . . . . . . . . . . . . 15 (𝑧 = (𝐹𝑤) → (𝑥𝐽𝑧) = (𝑥𝐽(𝐹𝑤)))
352351eleq2d 2823 . . . . . . . . . . . . . 14 (𝑧 = (𝐹𝑤) → (𝑦 ∈ (𝑥𝐽𝑧) ↔ 𝑦 ∈ (𝑥𝐽(𝐹𝑤))))
353 oveq2 7365 . . . . . . . . . . . . . . 15 (𝑧 = (𝐹𝑤) → (𝑦𝐸𝑧) = (𝑦𝐸(𝐹𝑤)))
354353eqeq1d 2738 . . . . . . . . . . . . . 14 (𝑧 = (𝐹𝑤) → ((𝑦𝐸𝑧) = (𝑎𝐸𝑏) ↔ (𝑦𝐸(𝐹𝑤)) = (𝑎𝐸𝑏)))
355352, 354anbi12d 631 . . . . . . . . . . . . 13 (𝑧 = (𝐹𝑤) → ((𝑦 ∈ (𝑥𝐽𝑧) ∧ (𝑦𝐸𝑧) = (𝑎𝐸𝑏)) ↔ (𝑦 ∈ (𝑥𝐽(𝐹𝑤)) ∧ (𝑦𝐸(𝐹𝑤)) = (𝑎𝐸𝑏))))
356355adantl 482 . . . . . . . . . . . 12 (((𝜑𝑤𝑃) ∧ 𝑧 = (𝐹𝑤)) → ((𝑦 ∈ (𝑥𝐽𝑧) ∧ (𝑦𝐸𝑧) = (𝑎𝐸𝑏)) ↔ (𝑦 ∈ (𝑥𝐽(𝐹𝑤)) ∧ (𝑦𝐸(𝐹𝑤)) = (𝑎𝐸𝑏))))
357336, 356rspcedv 3574 . . . . . . . . . . 11 ((𝜑𝑤𝑃) → ((𝑦 ∈ (𝑥𝐽(𝐹𝑤)) ∧ (𝑦𝐸(𝐹𝑤)) = (𝑎𝐸𝑏)) → ∃𝑧𝐵 (𝑦 ∈ (𝑥𝐽𝑧) ∧ (𝑦𝐸𝑧) = (𝑎𝐸𝑏))))
358357imp 407 . . . . . . . . . 10 (((𝜑𝑤𝑃) ∧ (𝑦 ∈ (𝑥𝐽(𝐹𝑤)) ∧ (𝑦𝐸(𝐹𝑤)) = (𝑎𝐸𝑏))) → ∃𝑧𝐵 (𝑦 ∈ (𝑥𝐽𝑧) ∧ (𝑦𝐸𝑧) = (𝑎𝐸𝑏)))
359325, 326, 340, 350, 358syl22anc 837 . . . . . . . . 9 (((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑎𝐵𝑏𝐵)) ∧ 𝑤𝑃) ∧ ((𝐹𝑦) ∈ ((𝐹𝑥)𝐼𝑤) ∧ ((𝐹𝑦)𝐷𝑤) = ((𝐹𝑎)𝐷(𝐹𝑏)))) → ∃𝑧𝐵 (𝑦 ∈ (𝑥𝐽𝑧) ∧ (𝑦𝐸𝑧) = (𝑎𝐸𝑏)))
3607adantr 481 . . . . . . . . . 10 (((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑎𝐵𝑏𝐵)) → 𝐺 ∈ TarskiG)
36113adantr 481 . . . . . . . . . 10 (((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑎𝐵𝑏𝐵)) → (𝐹𝑥) ∈ 𝑃)
36215adantr 481 . . . . . . . . . 10 (((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑎𝐵𝑏𝐵)) → (𝐹𝑦) ∈ 𝑃)
36311adantr 481 . . . . . . . . . . 11 (((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑎𝐵𝑏𝐵)) → 𝐹:𝐵𝑃)
364363, 345ffvelcdmd 7036 . . . . . . . . . 10 (((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑎𝐵𝑏𝐵)) → (𝐹𝑎) ∈ 𝑃)
365363, 347ffvelcdmd 7036 . . . . . . . . . 10 (((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑎𝐵𝑏𝐵)) → (𝐹𝑏) ∈ 𝑃)
3663, 4, 5, 360, 361, 362, 364, 365axtgsegcon 27406 . . . . . . . . 9 (((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑎𝐵𝑏𝐵)) → ∃𝑤𝑃 ((𝐹𝑦) ∈ ((𝐹𝑥)𝐼𝑤) ∧ ((𝐹𝑦)𝐷𝑤) = ((𝐹𝑎)𝐷(𝐹𝑏))))
367359, 366r19.29a 3159 . . . . . . . 8 (((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑎𝐵𝑏𝐵)) → ∃𝑧𝐵 (𝑦 ∈ (𝑥𝐽𝑧) ∧ (𝑦𝐸𝑧) = (𝑎𝐸𝑏)))
368367ralrimivva 3197 . . . . . . 7 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → ∀𝑎𝐵𝑏𝐵𝑧𝐵 (𝑦 ∈ (𝑥𝐽𝑧) ∧ (𝑦𝐸𝑧) = (𝑎𝐸𝑏)))
369368ralrimivva 3197 . . . . . 6 (𝜑 → ∀𝑥𝐵𝑦𝐵𝑎𝐵𝑏𝐵𝑧𝐵 (𝑦 ∈ (𝑥𝐽𝑧) ∧ (𝑦𝐸𝑧) = (𝑎𝐸𝑏)))
3702, 324, 369jca32 516 . . . . 5 (𝜑 → (𝐻 ∈ V ∧ (∀𝑥𝐵𝑦𝐵𝑧𝐵𝑢𝐵𝑎𝐵𝑏𝐵𝑐𝐵𝑣𝐵 (((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣)))) → (𝑧𝐸𝑢) = (𝑐𝐸𝑣)) ∧ ∀𝑥𝐵𝑦𝐵𝑎𝐵𝑏𝐵𝑧𝐵 (𝑦 ∈ (𝑥𝐽𝑧) ∧ (𝑦𝐸𝑧) = (𝑎𝐸𝑏)))))
37117, 18, 19istrkgcb 27398 . . . . 5 (𝐻 ∈ TarskiGCB ↔ (𝐻 ∈ V ∧ (∀𝑥𝐵𝑦𝐵𝑧𝐵𝑢𝐵𝑎𝐵𝑏𝐵𝑐𝐵𝑣𝐵 (((𝑥𝑦𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣)))) → (𝑧𝐸𝑢) = (𝑐𝐸𝑣)) ∧ ∀𝑥𝐵𝑦𝐵𝑎𝐵𝑏𝐵𝑧𝐵 (𝑦 ∈ (𝑥𝐽𝑧) ∧ (𝑦𝐸𝑧) = (𝑎𝐸𝑏)))))
372370, 371sylibr 233 . . . 4 (𝜑𝐻 ∈ TarskiGCB)
373 f1otrg.l . . . . 5 (𝜑 → (LineG‘𝐻) = (𝑥𝐵, 𝑦 ∈ (𝐵 ∖ {𝑥}) ↦ {𝑧𝐵 ∣ (𝑧 ∈ (𝑥𝐽𝑦) ∨ 𝑥 ∈ (𝑧𝐽𝑦) ∨ 𝑦 ∈ (𝑥𝐽𝑧))}))
37417, 18, 19istrkgl 27400 . . . . 5 (𝐻 ∈ {𝑓[(Base‘𝑓) / 𝑝][(Itv‘𝑓) / 𝑖](LineG‘𝑓) = (𝑥𝑝, 𝑦 ∈ (𝑝 ∖ {𝑥}) ↦ {𝑧𝑝 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})} ↔ (𝐻 ∈ V ∧ (LineG‘𝐻) = (𝑥𝐵, 𝑦 ∈ (𝐵 ∖ {𝑥}) ↦ {𝑧𝐵 ∣ (𝑧 ∈ (𝑥𝐽𝑦) ∨ 𝑥 ∈ (𝑧𝐽𝑦) ∨ 𝑦 ∈ (𝑥𝐽𝑧))})))
3752, 373, 374sylanbrc 583 . . . 4 (𝜑𝐻 ∈ {𝑓[(Base‘𝑓) / 𝑝][(Itv‘𝑓) / 𝑖](LineG‘𝑓) = (𝑥𝑝, 𝑦 ∈ (𝑝 ∖ {𝑥}) ↦ {𝑧𝑝 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})})
376372, 375elind 4154 . . 3 (𝜑𝐻 ∈ (TarskiGCB ∩ {𝑓[(Base‘𝑓) / 𝑝][(Itv‘𝑓) / 𝑖](LineG‘𝑓) = (𝑥𝑝, 𝑦 ∈ (𝑝 ∖ {𝑥}) ↦ {𝑧𝑝 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})}))
377252, 376elind 4154 . 2 (𝜑𝐻 ∈ ((TarskiGC ∩ TarskiGB) ∩ (TarskiGCB ∩ {𝑓[(Base‘𝑓) / 𝑝][(Itv‘𝑓) / 𝑖](LineG‘𝑓) = (𝑥𝑝, 𝑦 ∈ (𝑝 ∖ {𝑥}) ↦ {𝑧𝑝 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})})))
378 df-trkg 27395 . 2 TarskiG = ((TarskiGC ∩ TarskiGB) ∩ (TarskiGCB ∩ {𝑓[(Base‘𝑓) / 𝑝][(Itv‘𝑓) / 𝑖](LineG‘𝑓) = (𝑥𝑝, 𝑦 ∈ (𝑝 ∖ {𝑥}) ↦ {𝑧𝑝 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})}))
379377, 378eleqtrrdi 2849 1 (𝜑𝐻 ∈ TarskiG)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 396  w3o 1086  w3a 1087   = wceq 1541  wcel 2106  {cab 2713  wne 2943  wral 3064  wrex 3073  {crab 3407  Vcvv 3445  [wsbc 3739  cdif 3907  cin 3909  wss 3910  𝒫 cpw 4560  {csn 4586  ccnv 5632  ran crn 5634  cima 5636   Fn wfn 6491  wf 6492  1-1wf1 6493  ontowfo 6494  1-1-ontowf1o 6495  cfv 6496  (class class class)co 7357  cmpo 7359  Basecbs 17083  distcds 17142  TarskiGcstrkg 27369  TarskiGCcstrkgc 27370  TarskiGBcstrkgb 27371  TarskiGCBcstrkgcb 27372  Itvcitv 27375  LineGclng 27376
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707  ax-sep 5256  ax-nul 5263  ax-pr 5384
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-ne 2944  df-ral 3065  df-rex 3074  df-rab 3408  df-v 3447  df-sbc 3740  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-nul 4283  df-if 4487  df-pw 4562  df-sn 4587  df-pr 4589  df-op 4593  df-uni 4866  df-br 5106  df-opab 5168  df-id 5531  df-xp 5639  df-rel 5640  df-cnv 5641  df-co 5642  df-dm 5643  df-rn 5644  df-res 5645  df-ima 5646  df-iota 6448  df-fun 6498  df-fn 6499  df-f 6500  df-f1 6501  df-fo 6502  df-f1o 6503  df-fv 6504  df-ov 7360  df-oprab 7361  df-mpo 7362  df-trkgc 27390  df-trkgb 27391  df-trkgcb 27392  df-trkg 27395
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator