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

Theorem canthwelem 9662
 Description: Lemma for canthwe 9663. (Contributed by Mario Carneiro, 31-May-2015.)
Hypotheses
Ref Expression
canthwe.1 𝑂 = {⟨𝑥, 𝑟⟩ ∣ (𝑥𝐴𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥)}
canthwe.2 𝑊 = {⟨𝑥, 𝑟⟩ ∣ ((𝑥𝐴𝑟 ⊆ (𝑥 × 𝑥)) ∧ (𝑟 We 𝑥 ∧ ∀𝑦𝑥 [(𝑟 “ {𝑦}) / 𝑢](𝑢𝐹(𝑟 ∩ (𝑢 × 𝑢))) = 𝑦))}
canthwe.3 𝐵 = dom 𝑊
canthwe.4 𝐶 = ((𝑊𝐵) “ {(𝐵𝐹(𝑊𝐵))})
Assertion
Ref Expression
canthwelem (𝐴𝑉 → ¬ 𝐹:𝑂1-1𝐴)
Distinct variable groups:   𝑢,𝑟,𝑥,𝑦,𝐵   𝐶,𝑟,𝑥   𝑂,𝑟,𝑢,𝑥,𝑦   𝑉,𝑟,𝑢,𝑥,𝑦   𝐴,𝑟,𝑢,𝑥,𝑦   𝐹,𝑟,𝑢,𝑥,𝑦   𝑊,𝑟,𝑢,𝑥,𝑦
Allowed substitution hints:   𝐶(𝑦,𝑢)

Proof of Theorem canthwelem
StepHypRef Expression
1 eqid 2758 . . . . . . . 8 𝐵 = 𝐵
2 eqid 2758 . . . . . . . 8 (𝑊𝐵) = (𝑊𝐵)
31, 2pm3.2i 470 . . . . . . 7 (𝐵 = 𝐵 ∧ (𝑊𝐵) = (𝑊𝐵))
4 canthwe.2 . . . . . . . 8 𝑊 = {⟨𝑥, 𝑟⟩ ∣ ((𝑥𝐴𝑟 ⊆ (𝑥 × 𝑥)) ∧ (𝑟 We 𝑥 ∧ ∀𝑦𝑥 [(𝑟 “ {𝑦}) / 𝑢](𝑢𝐹(𝑟 ∩ (𝑢 × 𝑢))) = 𝑦))}
5 elex 3350 . . . . . . . . 9 (𝐴𝑉𝐴 ∈ V)
65adantr 472 . . . . . . . 8 ((𝐴𝑉𝐹:𝑂1-1𝐴) → 𝐴 ∈ V)
7 df-ov 6814 . . . . . . . . 9 (𝑥𝐹𝑟) = (𝐹‘⟨𝑥, 𝑟⟩)
8 f1f 6260 . . . . . . . . . . 11 (𝐹:𝑂1-1𝐴𝐹:𝑂𝐴)
98ad2antlr 765 . . . . . . . . . 10 (((𝐴𝑉𝐹:𝑂1-1𝐴) ∧ (𝑥𝐴𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥)) → 𝐹:𝑂𝐴)
10 simpr 479 . . . . . . . . . . . 12 (((𝐴𝑉𝐹:𝑂1-1𝐴) ∧ (𝑥𝐴𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥)) → (𝑥𝐴𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥))
11 opabid 5130 . . . . . . . . . . . 12 (⟨𝑥, 𝑟⟩ ∈ {⟨𝑥, 𝑟⟩ ∣ (𝑥𝐴𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥)} ↔ (𝑥𝐴𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥))
1210, 11sylibr 224 . . . . . . . . . . 11 (((𝐴𝑉𝐹:𝑂1-1𝐴) ∧ (𝑥𝐴𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥)) → ⟨𝑥, 𝑟⟩ ∈ {⟨𝑥, 𝑟⟩ ∣ (𝑥𝐴𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥)})
13 canthwe.1 . . . . . . . . . . 11 𝑂 = {⟨𝑥, 𝑟⟩ ∣ (𝑥𝐴𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥)}
1412, 13syl6eleqr 2848 . . . . . . . . . 10 (((𝐴𝑉𝐹:𝑂1-1𝐴) ∧ (𝑥𝐴𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥)) → ⟨𝑥, 𝑟⟩ ∈ 𝑂)
159, 14ffvelrnd 6521 . . . . . . . . 9 (((𝐴𝑉𝐹:𝑂1-1𝐴) ∧ (𝑥𝐴𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥)) → (𝐹‘⟨𝑥, 𝑟⟩) ∈ 𝐴)
167, 15syl5eqel 2841 . . . . . . . 8 (((𝐴𝑉𝐹:𝑂1-1𝐴) ∧ (𝑥𝐴𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥)) → (𝑥𝐹𝑟) ∈ 𝐴)
17 canthwe.3 . . . . . . . 8 𝐵 = dom 𝑊
184, 6, 16, 17fpwwe2 9655 . . . . . . 7 ((𝐴𝑉𝐹:𝑂1-1𝐴) → ((𝐵𝑊(𝑊𝐵) ∧ (𝐵𝐹(𝑊𝐵)) ∈ 𝐵) ↔ (𝐵 = 𝐵 ∧ (𝑊𝐵) = (𝑊𝐵))))
193, 18mpbiri 248 . . . . . 6 ((𝐴𝑉𝐹:𝑂1-1𝐴) → (𝐵𝑊(𝑊𝐵) ∧ (𝐵𝐹(𝑊𝐵)) ∈ 𝐵))
2019simprd 482 . . . . 5 ((𝐴𝑉𝐹:𝑂1-1𝐴) → (𝐵𝐹(𝑊𝐵)) ∈ 𝐵)
21 canthwe.4 . . . . . . . . . 10 𝐶 = ((𝑊𝐵) “ {(𝐵𝐹(𝑊𝐵))})
2221, 21xpeq12i 5292 . . . . . . . . . . 11 (𝐶 × 𝐶) = (((𝑊𝐵) “ {(𝐵𝐹(𝑊𝐵))}) × ((𝑊𝐵) “ {(𝐵𝐹(𝑊𝐵))}))
2322ineq2i 3952 . . . . . . . . . 10 ((𝑊𝐵) ∩ (𝐶 × 𝐶)) = ((𝑊𝐵) ∩ (((𝑊𝐵) “ {(𝐵𝐹(𝑊𝐵))}) × ((𝑊𝐵) “ {(𝐵𝐹(𝑊𝐵))})))
2421, 23oveq12i 6823 . . . . . . . . 9 (𝐶𝐹((𝑊𝐵) ∩ (𝐶 × 𝐶))) = (((𝑊𝐵) “ {(𝐵𝐹(𝑊𝐵))})𝐹((𝑊𝐵) ∩ (((𝑊𝐵) “ {(𝐵𝐹(𝑊𝐵))}) × ((𝑊𝐵) “ {(𝐵𝐹(𝑊𝐵))}))))
2519simpld 477 . . . . . . . . . . 11 ((𝐴𝑉𝐹:𝑂1-1𝐴) → 𝐵𝑊(𝑊𝐵))
264, 6, 25fpwwe2lem3 9645 . . . . . . . . . 10 (((𝐴𝑉𝐹:𝑂1-1𝐴) ∧ (𝐵𝐹(𝑊𝐵)) ∈ 𝐵) → (((𝑊𝐵) “ {(𝐵𝐹(𝑊𝐵))})𝐹((𝑊𝐵) ∩ (((𝑊𝐵) “ {(𝐵𝐹(𝑊𝐵))}) × ((𝑊𝐵) “ {(𝐵𝐹(𝑊𝐵))})))) = (𝐵𝐹(𝑊𝐵)))
2720, 26mpdan 705 . . . . . . . . 9 ((𝐴𝑉𝐹:𝑂1-1𝐴) → (((𝑊𝐵) “ {(𝐵𝐹(𝑊𝐵))})𝐹((𝑊𝐵) ∩ (((𝑊𝐵) “ {(𝐵𝐹(𝑊𝐵))}) × ((𝑊𝐵) “ {(𝐵𝐹(𝑊𝐵))})))) = (𝐵𝐹(𝑊𝐵)))
2824, 27syl5eq 2804 . . . . . . . 8 ((𝐴𝑉𝐹:𝑂1-1𝐴) → (𝐶𝐹((𝑊𝐵) ∩ (𝐶 × 𝐶))) = (𝐵𝐹(𝑊𝐵)))
29 df-ov 6814 . . . . . . . 8 (𝐶𝐹((𝑊𝐵) ∩ (𝐶 × 𝐶))) = (𝐹‘⟨𝐶, ((𝑊𝐵) ∩ (𝐶 × 𝐶))⟩)
30 df-ov 6814 . . . . . . . 8 (𝐵𝐹(𝑊𝐵)) = (𝐹‘⟨𝐵, (𝑊𝐵)⟩)
3128, 29, 303eqtr3g 2815 . . . . . . 7 ((𝐴𝑉𝐹:𝑂1-1𝐴) → (𝐹‘⟨𝐶, ((𝑊𝐵) ∩ (𝐶 × 𝐶))⟩) = (𝐹‘⟨𝐵, (𝑊𝐵)⟩))
32 simpr 479 . . . . . . . 8 ((𝐴𝑉𝐹:𝑂1-1𝐴) → 𝐹:𝑂1-1𝐴)
33 cnvimass 5641 . . . . . . . . . . . . 13 ((𝑊𝐵) “ {(𝐵𝐹(𝑊𝐵))}) ⊆ dom (𝑊𝐵)
344, 6fpwwe2lem2 9644 . . . . . . . . . . . . . . . . . 18 ((𝐴𝑉𝐹:𝑂1-1𝐴) → (𝐵𝑊(𝑊𝐵) ↔ ((𝐵𝐴 ∧ (𝑊𝐵) ⊆ (𝐵 × 𝐵)) ∧ ((𝑊𝐵) We 𝐵 ∧ ∀𝑦𝐵 [((𝑊𝐵) “ {𝑦}) / 𝑢](𝑢𝐹((𝑊𝐵) ∩ (𝑢 × 𝑢))) = 𝑦))))
3525, 34mpbid 222 . . . . . . . . . . . . . . . . 17 ((𝐴𝑉𝐹:𝑂1-1𝐴) → ((𝐵𝐴 ∧ (𝑊𝐵) ⊆ (𝐵 × 𝐵)) ∧ ((𝑊𝐵) We 𝐵 ∧ ∀𝑦𝐵 [((𝑊𝐵) “ {𝑦}) / 𝑢](𝑢𝐹((𝑊𝐵) ∩ (𝑢 × 𝑢))) = 𝑦)))
3635simpld 477 . . . . . . . . . . . . . . . 16 ((𝐴𝑉𝐹:𝑂1-1𝐴) → (𝐵𝐴 ∧ (𝑊𝐵) ⊆ (𝐵 × 𝐵)))
3736simprd 482 . . . . . . . . . . . . . . 15 ((𝐴𝑉𝐹:𝑂1-1𝐴) → (𝑊𝐵) ⊆ (𝐵 × 𝐵))
38 dmss 5476 . . . . . . . . . . . . . . 15 ((𝑊𝐵) ⊆ (𝐵 × 𝐵) → dom (𝑊𝐵) ⊆ dom (𝐵 × 𝐵))
3937, 38syl 17 . . . . . . . . . . . . . 14 ((𝐴𝑉𝐹:𝑂1-1𝐴) → dom (𝑊𝐵) ⊆ dom (𝐵 × 𝐵))
40 dmxpss 5721 . . . . . . . . . . . . . 14 dom (𝐵 × 𝐵) ⊆ 𝐵
4139, 40syl6ss 3754 . . . . . . . . . . . . 13 ((𝐴𝑉𝐹:𝑂1-1𝐴) → dom (𝑊𝐵) ⊆ 𝐵)
4233, 41syl5ss 3753 . . . . . . . . . . . 12 ((𝐴𝑉𝐹:𝑂1-1𝐴) → ((𝑊𝐵) “ {(𝐵𝐹(𝑊𝐵))}) ⊆ 𝐵)
4321, 42syl5eqss 3788 . . . . . . . . . . 11 ((𝐴𝑉𝐹:𝑂1-1𝐴) → 𝐶𝐵)
4436simpld 477 . . . . . . . . . . 11 ((𝐴𝑉𝐹:𝑂1-1𝐴) → 𝐵𝐴)
4543, 44sstrd 3752 . . . . . . . . . 10 ((𝐴𝑉𝐹:𝑂1-1𝐴) → 𝐶𝐴)
46 inss2 3975 . . . . . . . . . . 11 ((𝑊𝐵) ∩ (𝐶 × 𝐶)) ⊆ (𝐶 × 𝐶)
4746a1i 11 . . . . . . . . . 10 ((𝐴𝑉𝐹:𝑂1-1𝐴) → ((𝑊𝐵) ∩ (𝐶 × 𝐶)) ⊆ (𝐶 × 𝐶))
4835simprd 482 . . . . . . . . . . . . 13 ((𝐴𝑉𝐹:𝑂1-1𝐴) → ((𝑊𝐵) We 𝐵 ∧ ∀𝑦𝐵 [((𝑊𝐵) “ {𝑦}) / 𝑢](𝑢𝐹((𝑊𝐵) ∩ (𝑢 × 𝑢))) = 𝑦))
4948simpld 477 . . . . . . . . . . . 12 ((𝐴𝑉𝐹:𝑂1-1𝐴) → (𝑊𝐵) We 𝐵)
50 wess 5251 . . . . . . . . . . . 12 (𝐶𝐵 → ((𝑊𝐵) We 𝐵 → (𝑊𝐵) We 𝐶))
5143, 49, 50sylc 65 . . . . . . . . . . 11 ((𝐴𝑉𝐹:𝑂1-1𝐴) → (𝑊𝐵) We 𝐶)
52 weinxp 5341 . . . . . . . . . . 11 ((𝑊𝐵) We 𝐶 ↔ ((𝑊𝐵) ∩ (𝐶 × 𝐶)) We 𝐶)
5351, 52sylib 208 . . . . . . . . . 10 ((𝐴𝑉𝐹:𝑂1-1𝐴) → ((𝑊𝐵) ∩ (𝐶 × 𝐶)) We 𝐶)
54 fvex 6360 . . . . . . . . . . . . . 14 (𝑊𝐵) ∈ V
5554cnvex 7276 . . . . . . . . . . . . 13 (𝑊𝐵) ∈ V
5655imaex 7267 . . . . . . . . . . . 12 ((𝑊𝐵) “ {(𝐵𝐹(𝑊𝐵))}) ∈ V
5721, 56eqeltri 2833 . . . . . . . . . . 11 𝐶 ∈ V
5854inex1 4949 . . . . . . . . . . 11 ((𝑊𝐵) ∩ (𝐶 × 𝐶)) ∈ V
59 simpl 474 . . . . . . . . . . . . 13 ((𝑥 = 𝐶𝑟 = ((𝑊𝐵) ∩ (𝐶 × 𝐶))) → 𝑥 = 𝐶)
6059sseq1d 3771 . . . . . . . . . . . 12 ((𝑥 = 𝐶𝑟 = ((𝑊𝐵) ∩ (𝐶 × 𝐶))) → (𝑥𝐴𝐶𝐴))
61 simpr 479 . . . . . . . . . . . . 13 ((𝑥 = 𝐶𝑟 = ((𝑊𝐵) ∩ (𝐶 × 𝐶))) → 𝑟 = ((𝑊𝐵) ∩ (𝐶 × 𝐶)))
6259sqxpeqd 5296 . . . . . . . . . . . . 13 ((𝑥 = 𝐶𝑟 = ((𝑊𝐵) ∩ (𝐶 × 𝐶))) → (𝑥 × 𝑥) = (𝐶 × 𝐶))
6361, 62sseq12d 3773 . . . . . . . . . . . 12 ((𝑥 = 𝐶𝑟 = ((𝑊𝐵) ∩ (𝐶 × 𝐶))) → (𝑟 ⊆ (𝑥 × 𝑥) ↔ ((𝑊𝐵) ∩ (𝐶 × 𝐶)) ⊆ (𝐶 × 𝐶)))
64 weeq2 5253 . . . . . . . . . . . . 13 (𝑥 = 𝐶 → (𝑟 We 𝑥𝑟 We 𝐶))
65 weeq1 5252 . . . . . . . . . . . . 13 (𝑟 = ((𝑊𝐵) ∩ (𝐶 × 𝐶)) → (𝑟 We 𝐶 ↔ ((𝑊𝐵) ∩ (𝐶 × 𝐶)) We 𝐶))
6664, 65sylan9bb 738 . . . . . . . . . . . 12 ((𝑥 = 𝐶𝑟 = ((𝑊𝐵) ∩ (𝐶 × 𝐶))) → (𝑟 We 𝑥 ↔ ((𝑊𝐵) ∩ (𝐶 × 𝐶)) We 𝐶))
6760, 63, 663anbi123d 1546 . . . . . . . . . . 11 ((𝑥 = 𝐶𝑟 = ((𝑊𝐵) ∩ (𝐶 × 𝐶))) → ((𝑥𝐴𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥) ↔ (𝐶𝐴 ∧ ((𝑊𝐵) ∩ (𝐶 × 𝐶)) ⊆ (𝐶 × 𝐶) ∧ ((𝑊𝐵) ∩ (𝐶 × 𝐶)) We 𝐶)))
6857, 58, 67opelopaba 5139 . . . . . . . . . 10 (⟨𝐶, ((𝑊𝐵) ∩ (𝐶 × 𝐶))⟩ ∈ {⟨𝑥, 𝑟⟩ ∣ (𝑥𝐴𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥)} ↔ (𝐶𝐴 ∧ ((𝑊𝐵) ∩ (𝐶 × 𝐶)) ⊆ (𝐶 × 𝐶) ∧ ((𝑊𝐵) ∩ (𝐶 × 𝐶)) We 𝐶))
6945, 47, 53, 68syl3anbrc 1429 . . . . . . . . 9 ((𝐴𝑉𝐹:𝑂1-1𝐴) → ⟨𝐶, ((𝑊𝐵) ∩ (𝐶 × 𝐶))⟩ ∈ {⟨𝑥, 𝑟⟩ ∣ (𝑥𝐴𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥)})
7069, 13syl6eleqr 2848 . . . . . . . 8 ((𝐴𝑉𝐹:𝑂1-1𝐴) → ⟨𝐶, ((𝑊𝐵) ∩ (𝐶 × 𝐶))⟩ ∈ 𝑂)
716, 44ssexd 4955 . . . . . . . . . . 11 ((𝐴𝑉𝐹:𝑂1-1𝐴) → 𝐵 ∈ V)
7254a1i 11 . . . . . . . . . . 11 ((𝐴𝑉𝐹:𝑂1-1𝐴) → (𝑊𝐵) ∈ V)
73 simpl 474 . . . . . . . . . . . . . 14 ((𝑥 = 𝐵𝑟 = (𝑊𝐵)) → 𝑥 = 𝐵)
7473sseq1d 3771 . . . . . . . . . . . . 13 ((𝑥 = 𝐵𝑟 = (𝑊𝐵)) → (𝑥𝐴𝐵𝐴))
75 simpr 479 . . . . . . . . . . . . . 14 ((𝑥 = 𝐵𝑟 = (𝑊𝐵)) → 𝑟 = (𝑊𝐵))
7673sqxpeqd 5296 . . . . . . . . . . . . . 14 ((𝑥 = 𝐵𝑟 = (𝑊𝐵)) → (𝑥 × 𝑥) = (𝐵 × 𝐵))
7775, 76sseq12d 3773 . . . . . . . . . . . . 13 ((𝑥 = 𝐵𝑟 = (𝑊𝐵)) → (𝑟 ⊆ (𝑥 × 𝑥) ↔ (𝑊𝐵) ⊆ (𝐵 × 𝐵)))
78 weeq2 5253 . . . . . . . . . . . . . 14 (𝑥 = 𝐵 → (𝑟 We 𝑥𝑟 We 𝐵))
79 weeq1 5252 . . . . . . . . . . . . . 14 (𝑟 = (𝑊𝐵) → (𝑟 We 𝐵 ↔ (𝑊𝐵) We 𝐵))
8078, 79sylan9bb 738 . . . . . . . . . . . . 13 ((𝑥 = 𝐵𝑟 = (𝑊𝐵)) → (𝑟 We 𝑥 ↔ (𝑊𝐵) We 𝐵))
8174, 77, 803anbi123d 1546 . . . . . . . . . . . 12 ((𝑥 = 𝐵𝑟 = (𝑊𝐵)) → ((𝑥𝐴𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥) ↔ (𝐵𝐴 ∧ (𝑊𝐵) ⊆ (𝐵 × 𝐵) ∧ (𝑊𝐵) We 𝐵)))
8281opelopabga 5136 . . . . . . . . . . 11 ((𝐵 ∈ V ∧ (𝑊𝐵) ∈ V) → (⟨𝐵, (𝑊𝐵)⟩ ∈ {⟨𝑥, 𝑟⟩ ∣ (𝑥𝐴𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥)} ↔ (𝐵𝐴 ∧ (𝑊𝐵) ⊆ (𝐵 × 𝐵) ∧ (𝑊𝐵) We 𝐵)))
8371, 72, 82syl2anc 696 . . . . . . . . . 10 ((𝐴𝑉𝐹:𝑂1-1𝐴) → (⟨𝐵, (𝑊𝐵)⟩ ∈ {⟨𝑥, 𝑟⟩ ∣ (𝑥𝐴𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥)} ↔ (𝐵𝐴 ∧ (𝑊𝐵) ⊆ (𝐵 × 𝐵) ∧ (𝑊𝐵) We 𝐵)))
8444, 37, 49, 83mpbir3and 1428 . . . . . . . . 9 ((𝐴𝑉𝐹:𝑂1-1𝐴) → ⟨𝐵, (𝑊𝐵)⟩ ∈ {⟨𝑥, 𝑟⟩ ∣ (𝑥𝐴𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥)})
8584, 13syl6eleqr 2848 . . . . . . . 8 ((𝐴𝑉𝐹:𝑂1-1𝐴) → ⟨𝐵, (𝑊𝐵)⟩ ∈ 𝑂)
86 f1fveq 6680 . . . . . . . 8 ((𝐹:𝑂1-1𝐴 ∧ (⟨𝐶, ((𝑊𝐵) ∩ (𝐶 × 𝐶))⟩ ∈ 𝑂 ∧ ⟨𝐵, (𝑊𝐵)⟩ ∈ 𝑂)) → ((𝐹‘⟨𝐶, ((𝑊𝐵) ∩ (𝐶 × 𝐶))⟩) = (𝐹‘⟨𝐵, (𝑊𝐵)⟩) ↔ ⟨𝐶, ((𝑊𝐵) ∩ (𝐶 × 𝐶))⟩ = ⟨𝐵, (𝑊𝐵)⟩))
8732, 70, 85, 86syl12anc 1475 . . . . . . 7 ((𝐴𝑉𝐹:𝑂1-1𝐴) → ((𝐹‘⟨𝐶, ((𝑊𝐵) ∩ (𝐶 × 𝐶))⟩) = (𝐹‘⟨𝐵, (𝑊𝐵)⟩) ↔ ⟨𝐶, ((𝑊𝐵) ∩ (𝐶 × 𝐶))⟩ = ⟨𝐵, (𝑊𝐵)⟩))
8831, 87mpbid 222 . . . . . 6 ((𝐴𝑉𝐹:𝑂1-1𝐴) → ⟨𝐶, ((𝑊𝐵) ∩ (𝐶 × 𝐶))⟩ = ⟨𝐵, (𝑊𝐵)⟩)
8957, 58opth1 5090 . . . . . 6 (⟨𝐶, ((𝑊𝐵) ∩ (𝐶 × 𝐶))⟩ = ⟨𝐵, (𝑊𝐵)⟩ → 𝐶 = 𝐵)
9088, 89syl 17 . . . . 5 ((𝐴𝑉𝐹:𝑂1-1𝐴) → 𝐶 = 𝐵)
9120, 90eleqtrrd 2840 . . . 4 ((𝐴𝑉𝐹:𝑂1-1𝐴) → (𝐵𝐹(𝑊𝐵)) ∈ 𝐶)
9291, 21syl6eleq 2847 . . 3 ((𝐴𝑉𝐹:𝑂1-1𝐴) → (𝐵𝐹(𝑊𝐵)) ∈ ((𝑊𝐵) “ {(𝐵𝐹(𝑊𝐵))}))
93 ovex 6839 . . . . 5 (𝐵𝐹(𝑊𝐵)) ∈ V
9493eliniseg 5650 . . . 4 ((𝐵𝐹(𝑊𝐵)) ∈ 𝐵 → ((𝐵𝐹(𝑊𝐵)) ∈ ((𝑊𝐵) “ {(𝐵𝐹(𝑊𝐵))}) ↔ (𝐵𝐹(𝑊𝐵))(𝑊𝐵)(𝐵𝐹(𝑊𝐵))))
9520, 94syl 17 . . 3 ((𝐴𝑉𝐹:𝑂1-1𝐴) → ((𝐵𝐹(𝑊𝐵)) ∈ ((𝑊𝐵) “ {(𝐵𝐹(𝑊𝐵))}) ↔ (𝐵𝐹(𝑊𝐵))(𝑊𝐵)(𝐵𝐹(𝑊𝐵))))
9692, 95mpbid 222 . 2 ((𝐴𝑉𝐹:𝑂1-1𝐴) → (𝐵𝐹(𝑊𝐵))(𝑊𝐵)(𝐵𝐹(𝑊𝐵)))
97 weso 5255 . . . 4 ((𝑊𝐵) We 𝐵 → (𝑊𝐵) Or 𝐵)
9849, 97syl 17 . . 3 ((𝐴𝑉𝐹:𝑂1-1𝐴) → (𝑊𝐵) Or 𝐵)
99 sonr 5206 . . 3 (((𝑊𝐵) Or 𝐵 ∧ (𝐵𝐹(𝑊𝐵)) ∈ 𝐵) → ¬ (𝐵𝐹(𝑊𝐵))(𝑊𝐵)(𝐵𝐹(𝑊𝐵)))
10098, 20, 99syl2anc 696 . 2 ((𝐴𝑉𝐹:𝑂1-1𝐴) → ¬ (𝐵𝐹(𝑊𝐵))(𝑊𝐵)(𝐵𝐹(𝑊𝐵)))
10196, 100pm2.65da 601 1 (𝐴𝑉 → ¬ 𝐹:𝑂1-1𝐴)
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 196   ∧ wa 383   ∧ w3a 1072   = wceq 1630   ∈ wcel 2137  ∀wral 3048  Vcvv 3338  [wsbc 3574   ∩ cin 3712   ⊆ wss 3713  {csn 4319  ⟨cop 4325  ∪ cuni 4586   class class class wbr 4802  {copab 4862   Or wor 5184   We wwe 5222   × cxp 5262  ◡ccnv 5263  dom cdm 5264   “ cima 5267  ⟶wf 6043  –1-1→wf1 6044  ‘cfv 6047  (class class class)co 6811 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1869  ax-4 1884  ax-5 1986  ax-6 2052  ax-7 2088  ax-8 2139  ax-9 2146  ax-10 2166  ax-11 2181  ax-12 2194  ax-13 2389  ax-ext 2738  ax-rep 4921  ax-sep 4931  ax-nul 4939  ax-pow 4990  ax-pr 5053  ax-un 7112 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1633  df-ex 1852  df-nf 1857  df-sb 2045  df-eu 2609  df-mo 2610  df-clab 2745  df-cleq 2751  df-clel 2754  df-nfc 2889  df-ne 2931  df-ral 3053  df-rex 3054  df-reu 3055  df-rmo 3056  df-rab 3057  df-v 3340  df-sbc 3575  df-csb 3673  df-dif 3716  df-un 3718  df-in 3720  df-ss 3727  df-pss 3729  df-nul 4057  df-if 4229  df-pw 4302  df-sn 4320  df-pr 4322  df-tp 4324  df-op 4326  df-uni 4587  df-iun 4672  df-br 4803  df-opab 4863  df-mpt 4880  df-tr 4903  df-id 5172  df-eprel 5177  df-po 5185  df-so 5186  df-fr 5223  df-se 5224  df-we 5225  df-xp 5270  df-rel 5271  df-cnv 5272  df-co 5273  df-dm 5274  df-rn 5275  df-res 5276  df-ima 5277  df-pred 5839  df-ord 5885  df-on 5886  df-lim 5887  df-suc 5888  df-iota 6010  df-fun 6049  df-fn 6050  df-f 6051  df-f1 6052  df-fo 6053  df-f1o 6054  df-fv 6055  df-isom 6056  df-riota 6772  df-ov 6814  df-wrecs 7574  df-recs 7635  df-oi 8578 This theorem is referenced by:  canthwe  9663
 Copyright terms: Public domain W3C validator