Theorem canthwelem 10337

Description: Lemma for canthwe 10338. (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

Step	Hyp	Ref	Expression
1		eqid 2738	. . . . . . . 8 ⊢ 𝐵 = 𝐵
2		eqid 2738	. . . . . . . 8 ⊢ (𝑊‘𝐵) = (𝑊‘𝐵)
3	1, 2	pm3.2i 470	. . . . . . 7 ⊢ (𝐵 = 𝐵 ∧ (𝑊‘𝐵) = (𝑊‘𝐵))
4		canthwe.2	. . . . . . . 8 ⊢ 𝑊 = {⟨𝑥, 𝑟⟩ ∣ ((𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥)) ∧ (𝑟 We 𝑥 ∧ ∀𝑦 ∈ 𝑥 [(◡𝑟 “ {𝑦}) / 𝑢](𝑢𝐹(𝑟 ∩ (𝑢 × 𝑢))) = 𝑦))}
5		simpl 482	. . . . . . . 8 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝑂–1-1→𝐴) → 𝐴 ∈ 𝑉)
6		df-ov 7258	. . . . . . . . 9 ⊢ (𝑥𝐹𝑟) = (𝐹‘⟨𝑥, 𝑟⟩)
7		f1f 6654	. . . . . . . . . . 11 ⊢ (𝐹:𝑂–1-1→𝐴 → 𝐹:𝑂⟶𝐴)
8	7	ad2antlr 723	. . . . . . . . . 10 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹:𝑂–1-1→𝐴) ∧ (𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥)) → 𝐹:𝑂⟶𝐴)
9		simpr 484	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹:𝑂–1-1→𝐴) ∧ (𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥)) → (𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥))
10		opabidw 5431	. . . . . . . . . . . 12 ⊢ (⟨𝑥, 𝑟⟩ ∈ {⟨𝑥, 𝑟⟩ ∣ (𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥)} ↔ (𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥))
11	9, 10	sylibr 233	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹:𝑂–1-1→𝐴) ∧ (𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥)) → ⟨𝑥, 𝑟⟩ ∈ {⟨𝑥, 𝑟⟩ ∣ (𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥)})
12		canthwe.1	. . . . . . . . . . 11 ⊢ 𝑂 = {⟨𝑥, 𝑟⟩ ∣ (𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥)}
13	11, 12	eleqtrrdi 2850	. . . . . . . . . 10 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹:𝑂–1-1→𝐴) ∧ (𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥)) → ⟨𝑥, 𝑟⟩ ∈ 𝑂)
14	8, 13	ffvelrnd 6944	. . . . . . . . 9 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹:𝑂–1-1→𝐴) ∧ (𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥)) → (𝐹‘⟨𝑥, 𝑟⟩) ∈ 𝐴)
15	6, 14	eqeltrid 2843	. . . . . . . 8 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹:𝑂–1-1→𝐴) ∧ (𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥)) → (𝑥𝐹𝑟) ∈ 𝐴)
16		canthwe.3	. . . . . . . 8 ⊢ 𝐵 = ∪ dom 𝑊
17	4, 5, 15, 16	fpwwe2 10330	. . . . . . 7 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝑂–1-1→𝐴) → ((𝐵𝑊(𝑊‘𝐵) ∧ (𝐵𝐹(𝑊‘𝐵)) ∈ 𝐵) ↔ (𝐵 = 𝐵 ∧ (𝑊‘𝐵) = (𝑊‘𝐵))))
18	3, 17	mpbiri 257	. . . . . 6 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝑂–1-1→𝐴) → (𝐵𝑊(𝑊‘𝐵) ∧ (𝐵𝐹(𝑊‘𝐵)) ∈ 𝐵))
19	18	simprd 495	. . . . 5 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝑂–1-1→𝐴) → (𝐵𝐹(𝑊‘𝐵)) ∈ 𝐵)
20		canthwe.4	. . . . . . . . . 10 ⊢ 𝐶 = (◡(𝑊‘𝐵) “ {(𝐵𝐹(𝑊‘𝐵))})
21	20, 20	xpeq12i 5608	. . . . . . . . . . 11 ⊢ (𝐶 × 𝐶) = ((◡(𝑊‘𝐵) “ {(𝐵𝐹(𝑊‘𝐵))}) × (◡(𝑊‘𝐵) “ {(𝐵𝐹(𝑊‘𝐵))}))
22	21	ineq2i 4140	. . . . . . . . . 10 ⊢ ((𝑊‘𝐵) ∩ (𝐶 × 𝐶)) = ((𝑊‘𝐵) ∩ ((◡(𝑊‘𝐵) “ {(𝐵𝐹(𝑊‘𝐵))}) × (◡(𝑊‘𝐵) “ {(𝐵𝐹(𝑊‘𝐵))})))
23	20, 22	oveq12i 7267	. . . . . . . . 9 ⊢ (𝐶𝐹((𝑊‘𝐵) ∩ (𝐶 × 𝐶))) = ((◡(𝑊‘𝐵) “ {(𝐵𝐹(𝑊‘𝐵))})𝐹((𝑊‘𝐵) ∩ ((◡(𝑊‘𝐵) “ {(𝐵𝐹(𝑊‘𝐵))}) × (◡(𝑊‘𝐵) “ {(𝐵𝐹(𝑊‘𝐵))}))))
24	18	simpld 494	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝑂–1-1→𝐴) → 𝐵𝑊(𝑊‘𝐵))
25	4, 5, 24	fpwwe2lem3 10320	. . . . . . . . . 10 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹:𝑂–1-1→𝐴) ∧ (𝐵𝐹(𝑊‘𝐵)) ∈ 𝐵) → ((◡(𝑊‘𝐵) “ {(𝐵𝐹(𝑊‘𝐵))})𝐹((𝑊‘𝐵) ∩ ((◡(𝑊‘𝐵) “ {(𝐵𝐹(𝑊‘𝐵))}) × (◡(𝑊‘𝐵) “ {(𝐵𝐹(𝑊‘𝐵))})))) = (𝐵𝐹(𝑊‘𝐵)))
26	19, 25	mpdan 683	. . . . . . . . 9 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝑂–1-1→𝐴) → ((◡(𝑊‘𝐵) “ {(𝐵𝐹(𝑊‘𝐵))})𝐹((𝑊‘𝐵) ∩ ((◡(𝑊‘𝐵) “ {(𝐵𝐹(𝑊‘𝐵))}) × (◡(𝑊‘𝐵) “ {(𝐵𝐹(𝑊‘𝐵))})))) = (𝐵𝐹(𝑊‘𝐵)))
27	23, 26	eqtrid 2790	. . . . . . . 8 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝑂–1-1→𝐴) → (𝐶𝐹((𝑊‘𝐵) ∩ (𝐶 × 𝐶))) = (𝐵𝐹(𝑊‘𝐵)))
28		df-ov 7258	. . . . . . . 8 ⊢ (𝐶𝐹((𝑊‘𝐵) ∩ (𝐶 × 𝐶))) = (𝐹‘⟨𝐶, ((𝑊‘𝐵) ∩ (𝐶 × 𝐶))⟩)
29		df-ov 7258	. . . . . . . 8 ⊢ (𝐵𝐹(𝑊‘𝐵)) = (𝐹‘⟨𝐵, (𝑊‘𝐵)⟩)
30	27, 28, 29	3eqtr3g 2802	. . . . . . 7 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝑂–1-1→𝐴) → (𝐹‘⟨𝐶, ((𝑊‘𝐵) ∩ (𝐶 × 𝐶))⟩) = (𝐹‘⟨𝐵, (𝑊‘𝐵)⟩))
31		simpr 484	. . . . . . . 8 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝑂–1-1→𝐴) → 𝐹:𝑂–1-1→𝐴)
32		cnvimass 5978	. . . . . . . . . . . . 13 ⊢ (◡(𝑊‘𝐵) “ {(𝐵𝐹(𝑊‘𝐵))}) ⊆ dom (𝑊‘𝐵)
33	4, 5	fpwwe2lem2 10319	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝑂–1-1→𝐴) → (𝐵𝑊(𝑊‘𝐵) ↔ ((𝐵 ⊆ 𝐴 ∧ (𝑊‘𝐵) ⊆ (𝐵 × 𝐵)) ∧ ((𝑊‘𝐵) We 𝐵 ∧ ∀𝑦 ∈ 𝐵 [(◡(𝑊‘𝐵) “ {𝑦}) / 𝑢](𝑢𝐹((𝑊‘𝐵) ∩ (𝑢 × 𝑢))) = 𝑦))))
34	24, 33	mpbid 231	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝑂–1-1→𝐴) → ((𝐵 ⊆ 𝐴 ∧ (𝑊‘𝐵) ⊆ (𝐵 × 𝐵)) ∧ ((𝑊‘𝐵) We 𝐵 ∧ ∀𝑦 ∈ 𝐵 [(◡(𝑊‘𝐵) “ {𝑦}) / 𝑢](𝑢𝐹((𝑊‘𝐵) ∩ (𝑢 × 𝑢))) = 𝑦)))
35	34	simpld 494	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝑂–1-1→𝐴) → (𝐵 ⊆ 𝐴 ∧ (𝑊‘𝐵) ⊆ (𝐵 × 𝐵)))
36	35	simprd 495	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝑂–1-1→𝐴) → (𝑊‘𝐵) ⊆ (𝐵 × 𝐵))
37		dmss 5800	. . . . . . . . . . . . . . 15 ⊢ ((𝑊‘𝐵) ⊆ (𝐵 × 𝐵) → dom (𝑊‘𝐵) ⊆ dom (𝐵 × 𝐵))
38	36, 37	syl 17	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝑂–1-1→𝐴) → dom (𝑊‘𝐵) ⊆ dom (𝐵 × 𝐵))
39		dmxpss 6063	. . . . . . . . . . . . . 14 ⊢ dom (𝐵 × 𝐵) ⊆ 𝐵
40	38, 39	sstrdi 3929	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝑂–1-1→𝐴) → dom (𝑊‘𝐵) ⊆ 𝐵)
41	32, 40	sstrid 3928	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝑂–1-1→𝐴) → (◡(𝑊‘𝐵) “ {(𝐵𝐹(𝑊‘𝐵))}) ⊆ 𝐵)
42	20, 41	eqsstrid 3965	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝑂–1-1→𝐴) → 𝐶 ⊆ 𝐵)
43	35	simpld 494	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝑂–1-1→𝐴) → 𝐵 ⊆ 𝐴)
44	42, 43	sstrd 3927	. . . . . . . . . 10 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝑂–1-1→𝐴) → 𝐶 ⊆ 𝐴)
45		inss2 4160	. . . . . . . . . . 11 ⊢ ((𝑊‘𝐵) ∩ (𝐶 × 𝐶)) ⊆ (𝐶 × 𝐶)
46	45	a1i 11	. . . . . . . . . 10 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝑂–1-1→𝐴) → ((𝑊‘𝐵) ∩ (𝐶 × 𝐶)) ⊆ (𝐶 × 𝐶))
47	34	simprd 495	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝑂–1-1→𝐴) → ((𝑊‘𝐵) We 𝐵 ∧ ∀𝑦 ∈ 𝐵 [(◡(𝑊‘𝐵) “ {𝑦}) / 𝑢](𝑢𝐹((𝑊‘𝐵) ∩ (𝑢 × 𝑢))) = 𝑦))
48	47	simpld 494	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝑂–1-1→𝐴) → (𝑊‘𝐵) We 𝐵)
49		wess 5567	. . . . . . . . . . . 12 ⊢ (𝐶 ⊆ 𝐵 → ((𝑊‘𝐵) We 𝐵 → (𝑊‘𝐵) We 𝐶))
50	42, 48, 49	sylc 65	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝑂–1-1→𝐴) → (𝑊‘𝐵) We 𝐶)
51		weinxp 5662	. . . . . . . . . . 11 ⊢ ((𝑊‘𝐵) We 𝐶 ↔ ((𝑊‘𝐵) ∩ (𝐶 × 𝐶)) We 𝐶)
52	50, 51	sylib 217	. . . . . . . . . 10 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝑂–1-1→𝐴) → ((𝑊‘𝐵) ∩ (𝐶 × 𝐶)) We 𝐶)
53		fvex 6769	. . . . . . . . . . . . . 14 ⊢ (𝑊‘𝐵) ∈ V
54	53	cnvex 7746	. . . . . . . . . . . . 13 ⊢ ◡(𝑊‘𝐵) ∈ V
55	54	imaex 7737	. . . . . . . . . . . 12 ⊢ (◡(𝑊‘𝐵) “ {(𝐵𝐹(𝑊‘𝐵))}) ∈ V
56	20, 55	eqeltri 2835	. . . . . . . . . . 11 ⊢ 𝐶 ∈ V
57	53	inex1 5236	. . . . . . . . . . 11 ⊢ ((𝑊‘𝐵) ∩ (𝐶 × 𝐶)) ∈ V
58		simpl 482	. . . . . . . . . . . . 13 ⊢ ((𝑥 = 𝐶 ∧ 𝑟 = ((𝑊‘𝐵) ∩ (𝐶 × 𝐶))) → 𝑥 = 𝐶)
59	58	sseq1d 3948	. . . . . . . . . . . 12 ⊢ ((𝑥 = 𝐶 ∧ 𝑟 = ((𝑊‘𝐵) ∩ (𝐶 × 𝐶))) → (𝑥 ⊆ 𝐴 ↔ 𝐶 ⊆ 𝐴))
60		simpr 484	. . . . . . . . . . . . 13 ⊢ ((𝑥 = 𝐶 ∧ 𝑟 = ((𝑊‘𝐵) ∩ (𝐶 × 𝐶))) → 𝑟 = ((𝑊‘𝐵) ∩ (𝐶 × 𝐶)))
61	58	sqxpeqd 5612	. . . . . . . . . . . . 13 ⊢ ((𝑥 = 𝐶 ∧ 𝑟 = ((𝑊‘𝐵) ∩ (𝐶 × 𝐶))) → (𝑥 × 𝑥) = (𝐶 × 𝐶))
62	60, 61	sseq12d 3950	. . . . . . . . . . . 12 ⊢ ((𝑥 = 𝐶 ∧ 𝑟 = ((𝑊‘𝐵) ∩ (𝐶 × 𝐶))) → (𝑟 ⊆ (𝑥 × 𝑥) ↔ ((𝑊‘𝐵) ∩ (𝐶 × 𝐶)) ⊆ (𝐶 × 𝐶)))
63		weeq2 5569	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝐶 → (𝑟 We 𝑥 ↔ 𝑟 We 𝐶))
64		weeq1 5568	. . . . . . . . . . . . 13 ⊢ (𝑟 = ((𝑊‘𝐵) ∩ (𝐶 × 𝐶)) → (𝑟 We 𝐶 ↔ ((𝑊‘𝐵) ∩ (𝐶 × 𝐶)) We 𝐶))
65	63, 64	sylan9bb 509	. . . . . . . . . . . 12 ⊢ ((𝑥 = 𝐶 ∧ 𝑟 = ((𝑊‘𝐵) ∩ (𝐶 × 𝐶))) → (𝑟 We 𝑥 ↔ ((𝑊‘𝐵) ∩ (𝐶 × 𝐶)) We 𝐶))
66	59, 62, 65	3anbi123d 1434	. . . . . . . . . . 11 ⊢ ((𝑥 = 𝐶 ∧ 𝑟 = ((𝑊‘𝐵) ∩ (𝐶 × 𝐶))) → ((𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥) ↔ (𝐶 ⊆ 𝐴 ∧ ((𝑊‘𝐵) ∩ (𝐶 × 𝐶)) ⊆ (𝐶 × 𝐶) ∧ ((𝑊‘𝐵) ∩ (𝐶 × 𝐶)) We 𝐶)))
67	56, 57, 66	opelopaba 5442	. . . . . . . . . 10 ⊢ (⟨𝐶, ((𝑊‘𝐵) ∩ (𝐶 × 𝐶))⟩ ∈ {⟨𝑥, 𝑟⟩ ∣ (𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥)} ↔ (𝐶 ⊆ 𝐴 ∧ ((𝑊‘𝐵) ∩ (𝐶 × 𝐶)) ⊆ (𝐶 × 𝐶) ∧ ((𝑊‘𝐵) ∩ (𝐶 × 𝐶)) We 𝐶))
68	44, 46, 52, 67	syl3anbrc 1341	. . . . . . . . 9 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝑂–1-1→𝐴) → ⟨𝐶, ((𝑊‘𝐵) ∩ (𝐶 × 𝐶))⟩ ∈ {⟨𝑥, 𝑟⟩ ∣ (𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥)})
69	68, 12	eleqtrrdi 2850	. . . . . . . 8 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝑂–1-1→𝐴) → ⟨𝐶, ((𝑊‘𝐵) ∩ (𝐶 × 𝐶))⟩ ∈ 𝑂)
70	5, 43	ssexd 5243	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝑂–1-1→𝐴) → 𝐵 ∈ V)
71	53	a1i 11	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝑂–1-1→𝐴) → (𝑊‘𝐵) ∈ V)
72		simpl 482	. . . . . . . . . . . . . 14 ⊢ ((𝑥 = 𝐵 ∧ 𝑟 = (𝑊‘𝐵)) → 𝑥 = 𝐵)
73	72	sseq1d 3948	. . . . . . . . . . . . 13 ⊢ ((𝑥 = 𝐵 ∧ 𝑟 = (𝑊‘𝐵)) → (𝑥 ⊆ 𝐴 ↔ 𝐵 ⊆ 𝐴))
74		simpr 484	. . . . . . . . . . . . . 14 ⊢ ((𝑥 = 𝐵 ∧ 𝑟 = (𝑊‘𝐵)) → 𝑟 = (𝑊‘𝐵))
75	72	sqxpeqd 5612	. . . . . . . . . . . . . 14 ⊢ ((𝑥 = 𝐵 ∧ 𝑟 = (𝑊‘𝐵)) → (𝑥 × 𝑥) = (𝐵 × 𝐵))
76	74, 75	sseq12d 3950	. . . . . . . . . . . . 13 ⊢ ((𝑥 = 𝐵 ∧ 𝑟 = (𝑊‘𝐵)) → (𝑟 ⊆ (𝑥 × 𝑥) ↔ (𝑊‘𝐵) ⊆ (𝐵 × 𝐵)))
77		weeq2 5569	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝐵 → (𝑟 We 𝑥 ↔ 𝑟 We 𝐵))
78		weeq1 5568	. . . . . . . . . . . . . 14 ⊢ (𝑟 = (𝑊‘𝐵) → (𝑟 We 𝐵 ↔ (𝑊‘𝐵) We 𝐵))
79	77, 78	sylan9bb 509	. . . . . . . . . . . . 13 ⊢ ((𝑥 = 𝐵 ∧ 𝑟 = (𝑊‘𝐵)) → (𝑟 We 𝑥 ↔ (𝑊‘𝐵) We 𝐵))
80	73, 76, 79	3anbi123d 1434	. . . . . . . . . . . 12 ⊢ ((𝑥 = 𝐵 ∧ 𝑟 = (𝑊‘𝐵)) → ((𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥) ↔ (𝐵 ⊆ 𝐴 ∧ (𝑊‘𝐵) ⊆ (𝐵 × 𝐵) ∧ (𝑊‘𝐵) We 𝐵)))
81	80	opelopabga 5439	. . . . . . . . . . 11 ⊢ ((𝐵 ∈ V ∧ (𝑊‘𝐵) ∈ V) → (⟨𝐵, (𝑊‘𝐵)⟩ ∈ {⟨𝑥, 𝑟⟩ ∣ (𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥)} ↔ (𝐵 ⊆ 𝐴 ∧ (𝑊‘𝐵) ⊆ (𝐵 × 𝐵) ∧ (𝑊‘𝐵) We 𝐵)))
82	70, 71, 81	syl2anc 583	. . . . . . . . . 10 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝑂–1-1→𝐴) → (⟨𝐵, (𝑊‘𝐵)⟩ ∈ {⟨𝑥, 𝑟⟩ ∣ (𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥)} ↔ (𝐵 ⊆ 𝐴 ∧ (𝑊‘𝐵) ⊆ (𝐵 × 𝐵) ∧ (𝑊‘𝐵) We 𝐵)))
83	43, 36, 48, 82	mpbir3and 1340	. . . . . . . . 9 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝑂–1-1→𝐴) → ⟨𝐵, (𝑊‘𝐵)⟩ ∈ {⟨𝑥, 𝑟⟩ ∣ (𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥)})
84	83, 12	eleqtrrdi 2850	. . . . . . . 8 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝑂–1-1→𝐴) → ⟨𝐵, (𝑊‘𝐵)⟩ ∈ 𝑂)
85		f1fveq 7116	. . . . . . . 8 ⊢ ((𝐹:𝑂–1-1→𝐴 ∧ (⟨𝐶, ((𝑊‘𝐵) ∩ (𝐶 × 𝐶))⟩ ∈ 𝑂 ∧ ⟨𝐵, (𝑊‘𝐵)⟩ ∈ 𝑂)) → ((𝐹‘⟨𝐶, ((𝑊‘𝐵) ∩ (𝐶 × 𝐶))⟩) = (𝐹‘⟨𝐵, (𝑊‘𝐵)⟩) ↔ ⟨𝐶, ((𝑊‘𝐵) ∩ (𝐶 × 𝐶))⟩ = ⟨𝐵, (𝑊‘𝐵)⟩))
86	31, 69, 84, 85	syl12anc 833	. . . . . . 7 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝑂–1-1→𝐴) → ((𝐹‘⟨𝐶, ((𝑊‘𝐵) ∩ (𝐶 × 𝐶))⟩) = (𝐹‘⟨𝐵, (𝑊‘𝐵)⟩) ↔ ⟨𝐶, ((𝑊‘𝐵) ∩ (𝐶 × 𝐶))⟩ = ⟨𝐵, (𝑊‘𝐵)⟩))
87	30, 86	mpbid 231	. . . . . 6 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝑂–1-1→𝐴) → ⟨𝐶, ((𝑊‘𝐵) ∩ (𝐶 × 𝐶))⟩ = ⟨𝐵, (𝑊‘𝐵)⟩)
88	56, 57	opth1 5384	. . . . . 6 ⊢ (⟨𝐶, ((𝑊‘𝐵) ∩ (𝐶 × 𝐶))⟩ = ⟨𝐵, (𝑊‘𝐵)⟩ → 𝐶 = 𝐵)
89	87, 88	syl 17	. . . . 5 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝑂–1-1→𝐴) → 𝐶 = 𝐵)
90	19, 89	eleqtrrd 2842	. . . 4 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝑂–1-1→𝐴) → (𝐵𝐹(𝑊‘𝐵)) ∈ 𝐶)
91	90, 20	eleqtrdi 2849	. . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝑂–1-1→𝐴) → (𝐵𝐹(𝑊‘𝐵)) ∈ (◡(𝑊‘𝐵) “ {(𝐵𝐹(𝑊‘𝐵))}))
92		ovex 7288	. . . . 5 ⊢ (𝐵𝐹(𝑊‘𝐵)) ∈ V
93	92	eliniseg 5991	. . . 4 ⊢ ((𝐵𝐹(𝑊‘𝐵)) ∈ 𝐵 → ((𝐵𝐹(𝑊‘𝐵)) ∈ (◡(𝑊‘𝐵) “ {(𝐵𝐹(𝑊‘𝐵))}) ↔ (𝐵𝐹(𝑊‘𝐵))(𝑊‘𝐵)(𝐵𝐹(𝑊‘𝐵))))
94	19, 93	syl 17	. . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝑂–1-1→𝐴) → ((𝐵𝐹(𝑊‘𝐵)) ∈ (◡(𝑊‘𝐵) “ {(𝐵𝐹(𝑊‘𝐵))}) ↔ (𝐵𝐹(𝑊‘𝐵))(𝑊‘𝐵)(𝐵𝐹(𝑊‘𝐵))))
95	91, 94	mpbid 231	. 2 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝑂–1-1→𝐴) → (𝐵𝐹(𝑊‘𝐵))(𝑊‘𝐵)(𝐵𝐹(𝑊‘𝐵)))
96		weso 5571	. . . 4 ⊢ ((𝑊‘𝐵) We 𝐵 → (𝑊‘𝐵) Or 𝐵)
97	48, 96	syl 17	. . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝑂–1-1→𝐴) → (𝑊‘𝐵) Or 𝐵)
98		sonr 5517	. . 3 ⊢ (((𝑊‘𝐵) Or 𝐵 ∧ (𝐵𝐹(𝑊‘𝐵)) ∈ 𝐵) → ¬ (𝐵𝐹(𝑊‘𝐵))(𝑊‘𝐵)(𝐵𝐹(𝑊‘𝐵)))
99	97, 19, 98	syl2anc 583	. 2 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝑂–1-1→𝐴) → ¬ (𝐵𝐹(𝑊‘𝐵))(𝑊‘𝐵)(𝐵𝐹(𝑊‘𝐵)))
100	95, 99	pm2.65da 813	1 ⊢ (𝐴 ∈ 𝑉 → ¬ 𝐹:𝑂–1-1→𝐴)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∧ wa 395   ∧ w3a 1085   = wceq 1539   ∈ wcel 2108  ∀wral 3063  Vcvv 3422  [wsbc 3711   ∩ cin 3882   ⊆ wss 3883  {csn 4558  ⟨cop 4564  ∪ cuni 4836   class class class wbr 5070  {copab 5132   Or wor 5493   We wwe 5534   × cxp 5578  ^◡ccnv 5579  dom cdm 5580   “ cima 5583  ⟶wf 6414  –1-1→wf1 6415  ‘cfv 6418  (class class class)co 7255

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709  ax-rep 5205  ax-sep 5218  ax-nul 5225  ax-pow 5283  ax-pr 5347  ax-un 7566

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2888  df-ne 2943  df-ral 3068  df-rex 3069  df-reu 3070  df-rmo 3071  df-rab 3072  df-v 3424  df-sbc 3712  df-csb 3829  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-pss 3902  df-nul 4254  df-if 4457  df-pw 4532  df-sn 4559  df-pr 4561  df-tp 4563  df-op 4565  df-uni 4837  df-iun 4923  df-br 5071  df-opab 5133  df-mpt 5154  df-tr 5188  df-id 5480  df-eprel 5486  df-po 5494  df-so 5495  df-fr 5535  df-se 5536  df-we 5537  df-xp 5586  df-rel 5587  df-cnv 5588  df-co 5589  df-dm 5590  df-rn 5591  df-res 5592  df-ima 5593  df-pred 6191  df-ord 6254  df-on 6255  df-lim 6256  df-suc 6257  df-iota 6376  df-fun 6420  df-fn 6421  df-f 6422  df-f1 6423  df-fo 6424  df-f1o 6425  df-fv 6426  df-isom 6427  df-riota 7212  df-ov 7258  df-2nd 7805  df-frecs 8068  df-wrecs 8099  df-recs 8173  df-oi 9199

This theorem is referenced by:  canthwe  10338