Metamath Proof Explorer

Theorem canthwelem

Description: Lemma for canthwe . (Contributed by Mario Carneiro, 31-May-2015)

Ref Expression
Hypotheses canthwe.1 ⊢ 𝑂 = { ⟨ 𝑥 , 𝑟 ⟩ ∣ ( 𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ ( 𝑥 × 𝑥 ) ∧ 𝑟 We 𝑥 ) }
canthwe.2 ⊢ 𝑊 = { ⟨ 𝑥 , 𝑟 ⟩ ∣ ( ( 𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ ( 𝑥 × 𝑥 ) ) ∧ ( 𝑟 We 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 [ ( ◡ 𝑟 “ { 𝑦 } ) / 𝑢 ] ( 𝑢 𝐹 ( 𝑟 ∩ ( 𝑢 × 𝑢 ) ) ) = 𝑦 ) ) }
canthwe.3 ⊢ 𝐵 = ∪ dom 𝑊
canthwe.4 ⊢ 𝐶 = ( ◡ ( 𝑊 ‘ 𝐵 ) “ { ( 𝐵 𝐹 ( 𝑊 ‘ 𝐵 ) ) } )
Assertion canthwelem ( 𝐴 ∈ 𝑉 → ¬ 𝐹 : 𝑂 –1-1→ 𝐴 )

Proof

Step Hyp Ref Expression
1 canthwe.1 ⊢ 𝑂 = { ⟨ 𝑥 , 𝑟 ⟩ ∣ ( 𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ ( 𝑥 × 𝑥 ) ∧ 𝑟 We 𝑥 ) }
2 canthwe.2 ⊢ 𝑊 = { ⟨ 𝑥 , 𝑟 ⟩ ∣ ( ( 𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ ( 𝑥 × 𝑥 ) ) ∧ ( 𝑟 We 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 [ ( ◡ 𝑟 “ { 𝑦 } ) / 𝑢 ] ( 𝑢 𝐹 ( 𝑟 ∩ ( 𝑢 × 𝑢 ) ) ) = 𝑦 ) ) }
3 canthwe.3 ⊢ 𝐵 = ∪ dom 𝑊
4 canthwe.4 ⊢ 𝐶 = ( ◡ ( 𝑊 ‘ 𝐵 ) “ { ( 𝐵 𝐹 ( 𝑊 ‘ 𝐵 ) ) } )
5 eqid ⊢ 𝐵 = 𝐵
6 eqid ⊢ ( 𝑊 ‘ 𝐵 ) = ( 𝑊 ‘ 𝐵 )
7 5 6 pm3.2i ⊢ ( 𝐵 = 𝐵 ∧ ( 𝑊 ‘ 𝐵 ) = ( 𝑊 ‘ 𝐵 ) )
8 simpl ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝑂 –1-1→ 𝐴 ) → 𝐴 ∈ 𝑉 )
9 df-ov ⊢ ( 𝑥 𝐹 𝑟 ) = ( 𝐹 ‘ ⟨ 𝑥 , 𝑟 ⟩ )
10 f1f ⊢ ( 𝐹 : 𝑂 –1-1→ 𝐴 → 𝐹 : 𝑂 ⟶ 𝐴 )
11 10 ad2antlr ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝑂 –1-1→ 𝐴 ) ∧ ( 𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ ( 𝑥 × 𝑥 ) ∧ 𝑟 We 𝑥 ) ) → 𝐹 : 𝑂 ⟶ 𝐴 )
12 opabidw ⊢ ( ⟨ 𝑥 , 𝑟 ⟩ ∈ { ⟨ 𝑥 , 𝑟 ⟩ ∣ ( 𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ ( 𝑥 × 𝑥 ) ∧ 𝑟 We 𝑥 ) } ↔ ( 𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ ( 𝑥 × 𝑥 ) ∧ 𝑟 We 𝑥 ) )
13 12 bilanri ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝑂 –1-1→ 𝐴 ) ∧ ( 𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ ( 𝑥 × 𝑥 ) ∧ 𝑟 We 𝑥 ) ) → ⟨ 𝑥 , 𝑟 ⟩ ∈ { ⟨ 𝑥 , 𝑟 ⟩ ∣ ( 𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ ( 𝑥 × 𝑥 ) ∧ 𝑟 We 𝑥 ) } )
14 13 1 eleqtrrdi ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝑂 –1-1→ 𝐴 ) ∧ ( 𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ ( 𝑥 × 𝑥 ) ∧ 𝑟 We 𝑥 ) ) → ⟨ 𝑥 , 𝑟 ⟩ ∈ 𝑂 )
15 11 14 ffvelcdmd ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝑂 –1-1→ 𝐴 ) ∧ ( 𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ ( 𝑥 × 𝑥 ) ∧ 𝑟 We 𝑥 ) ) → ( 𝐹 ‘ ⟨ 𝑥 , 𝑟 ⟩ ) ∈ 𝐴 )
16 9 15 eqeltrid ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝑂 –1-1→ 𝐴 ) ∧ ( 𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ ( 𝑥 × 𝑥 ) ∧ 𝑟 We 𝑥 ) ) → ( 𝑥 𝐹 𝑟 ) ∈ 𝐴 )
17 2 8 16 3 fpwwe2 ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝑂 –1-1→ 𝐴 ) → ( ( 𝐵 𝑊 ( 𝑊 ‘ 𝐵 ) ∧ ( 𝐵 𝐹 ( 𝑊 ‘ 𝐵 ) ) ∈ 𝐵 ) ↔ ( 𝐵 = 𝐵 ∧ ( 𝑊 ‘ 𝐵 ) = ( 𝑊 ‘ 𝐵 ) ) ) )
18 7 17 mpbiri ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝑂 –1-1→ 𝐴 ) → ( 𝐵 𝑊 ( 𝑊 ‘ 𝐵 ) ∧ ( 𝐵 𝐹 ( 𝑊 ‘ 𝐵 ) ) ∈ 𝐵 ) )
19 18 simprd ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝑂 –1-1→ 𝐴 ) → ( 𝐵 𝐹 ( 𝑊 ‘ 𝐵 ) ) ∈ 𝐵 )
20 4 4 xpeq12i ⊢ ( 𝐶 × 𝐶 ) = ( ( ◡ ( 𝑊 ‘ 𝐵 ) “ { ( 𝐵 𝐹 ( 𝑊 ‘ 𝐵 ) ) } ) × ( ◡ ( 𝑊 ‘ 𝐵 ) “ { ( 𝐵 𝐹 ( 𝑊 ‘ 𝐵 ) ) } ) )
21 20 ineq2i ⊢ ( ( 𝑊 ‘ 𝐵 ) ∩ ( 𝐶 × 𝐶 ) ) = ( ( 𝑊 ‘ 𝐵 ) ∩ ( ( ◡ ( 𝑊 ‘ 𝐵 ) “ { ( 𝐵 𝐹 ( 𝑊 ‘ 𝐵 ) ) } ) × ( ◡ ( 𝑊 ‘ 𝐵 ) “ { ( 𝐵 𝐹 ( 𝑊 ‘ 𝐵 ) ) } ) ) )
22 4 21 oveq12i ⊢ ( 𝐶 𝐹 ( ( 𝑊 ‘ 𝐵 ) ∩ ( 𝐶 × 𝐶 ) ) ) = ( ( ◡ ( 𝑊 ‘ 𝐵 ) “ { ( 𝐵 𝐹 ( 𝑊 ‘ 𝐵 ) ) } ) 𝐹 ( ( 𝑊 ‘ 𝐵 ) ∩ ( ( ◡ ( 𝑊 ‘ 𝐵 ) “ { ( 𝐵 𝐹 ( 𝑊 ‘ 𝐵 ) ) } ) × ( ◡ ( 𝑊 ‘ 𝐵 ) “ { ( 𝐵 𝐹 ( 𝑊 ‘ 𝐵 ) ) } ) ) ) )
23 18 simpld ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝑂 –1-1→ 𝐴 ) → 𝐵 𝑊 ( 𝑊 ‘ 𝐵 ) )
24 2 8 23 fpwwe2lem3 ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝑂 –1-1→ 𝐴 ) ∧ ( 𝐵 𝐹 ( 𝑊 ‘ 𝐵 ) ) ∈ 𝐵 ) → ( ( ◡ ( 𝑊 ‘ 𝐵 ) “ { ( 𝐵 𝐹 ( 𝑊 ‘ 𝐵 ) ) } ) 𝐹 ( ( 𝑊 ‘ 𝐵 ) ∩ ( ( ◡ ( 𝑊 ‘ 𝐵 ) “ { ( 𝐵 𝐹 ( 𝑊 ‘ 𝐵 ) ) } ) × ( ◡ ( 𝑊 ‘ 𝐵 ) “ { ( 𝐵 𝐹 ( 𝑊 ‘ 𝐵 ) ) } ) ) ) ) = ( 𝐵 𝐹 ( 𝑊 ‘ 𝐵 ) ) )
25 19 24 mpdan ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝑂 –1-1→ 𝐴 ) → ( ( ◡ ( 𝑊 ‘ 𝐵 ) “ { ( 𝐵 𝐹 ( 𝑊 ‘ 𝐵 ) ) } ) 𝐹 ( ( 𝑊 ‘ 𝐵 ) ∩ ( ( ◡ ( 𝑊 ‘ 𝐵 ) “ { ( 𝐵 𝐹 ( 𝑊 ‘ 𝐵 ) ) } ) × ( ◡ ( 𝑊 ‘ 𝐵 ) “ { ( 𝐵 𝐹 ( 𝑊 ‘ 𝐵 ) ) } ) ) ) ) = ( 𝐵 𝐹 ( 𝑊 ‘ 𝐵 ) ) )
26 22 25 eqtrid ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝑂 –1-1→ 𝐴 ) → ( 𝐶 𝐹 ( ( 𝑊 ‘ 𝐵 ) ∩ ( 𝐶 × 𝐶 ) ) ) = ( 𝐵 𝐹 ( 𝑊 ‘ 𝐵 ) ) )
27 df-ov ⊢ ( 𝐶 𝐹 ( ( 𝑊 ‘ 𝐵 ) ∩ ( 𝐶 × 𝐶 ) ) ) = ( 𝐹 ‘ ⟨ 𝐶 , ( ( 𝑊 ‘ 𝐵 ) ∩ ( 𝐶 × 𝐶 ) ) ⟩ )
28 df-ov ⊢ ( 𝐵 𝐹 ( 𝑊 ‘ 𝐵 ) ) = ( 𝐹 ‘ ⟨ 𝐵 , ( 𝑊 ‘ 𝐵 ) ⟩ )
29 26 27 28 3eqtr3g ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝑂 –1-1→ 𝐴 ) → ( 𝐹 ‘ ⟨ 𝐶 , ( ( 𝑊 ‘ 𝐵 ) ∩ ( 𝐶 × 𝐶 ) ) ⟩ ) = ( 𝐹 ‘ ⟨ 𝐵 , ( 𝑊 ‘ 𝐵 ) ⟩ ) )
30 simpr ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝑂 –1-1→ 𝐴 ) → 𝐹 : 𝑂 –1-1→ 𝐴 )
31 cnvimass ⊢ ( ◡ ( 𝑊 ‘ 𝐵 ) “ { ( 𝐵 𝐹 ( 𝑊 ‘ 𝐵 ) ) } ) ⊆ dom ( 𝑊 ‘ 𝐵 )
32 2 8 fpwwe2lem2 ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝑂 –1-1→ 𝐴 ) → ( 𝐵 𝑊 ( 𝑊 ‘ 𝐵 ) ↔ ( ( 𝐵 ⊆ 𝐴 ∧ ( 𝑊 ‘ 𝐵 ) ⊆ ( 𝐵 × 𝐵 ) ) ∧ ( ( 𝑊 ‘ 𝐵 ) We 𝐵 ∧ ∀ 𝑦 ∈ 𝐵 [ ( ◡ ( 𝑊 ‘ 𝐵 ) “ { 𝑦 } ) / 𝑢 ] ( 𝑢 𝐹 ( ( 𝑊 ‘ 𝐵 ) ∩ ( 𝑢 × 𝑢 ) ) ) = 𝑦 ) ) ) )
33 23 32 mpbid ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝑂 –1-1→ 𝐴 ) → ( ( 𝐵 ⊆ 𝐴 ∧ ( 𝑊 ‘ 𝐵 ) ⊆ ( 𝐵 × 𝐵 ) ) ∧ ( ( 𝑊 ‘ 𝐵 ) We 𝐵 ∧ ∀ 𝑦 ∈ 𝐵 [ ( ◡ ( 𝑊 ‘ 𝐵 ) “ { 𝑦 } ) / 𝑢 ] ( 𝑢 𝐹 ( ( 𝑊 ‘ 𝐵 ) ∩ ( 𝑢 × 𝑢 ) ) ) = 𝑦 ) ) )
34 33 simpld ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝑂 –1-1→ 𝐴 ) → ( 𝐵 ⊆ 𝐴 ∧ ( 𝑊 ‘ 𝐵 ) ⊆ ( 𝐵 × 𝐵 ) ) )
35 34 simprd ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝑂 –1-1→ 𝐴 ) → ( 𝑊 ‘ 𝐵 ) ⊆ ( 𝐵 × 𝐵 ) )
36 dmss ⊢ ( ( 𝑊 ‘ 𝐵 ) ⊆ ( 𝐵 × 𝐵 ) → dom ( 𝑊 ‘ 𝐵 ) ⊆ dom ( 𝐵 × 𝐵 ) )
37 35 36 syl ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝑂 –1-1→ 𝐴 ) → dom ( 𝑊 ‘ 𝐵 ) ⊆ dom ( 𝐵 × 𝐵 ) )
38 dmxpss ⊢ dom ( 𝐵 × 𝐵 ) ⊆ 𝐵
39 37 38 sstrdi ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝑂 –1-1→ 𝐴 ) → dom ( 𝑊 ‘ 𝐵 ) ⊆ 𝐵 )
40 31 39 sstrid ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝑂 –1-1→ 𝐴 ) → ( ◡ ( 𝑊 ‘ 𝐵 ) “ { ( 𝐵 𝐹 ( 𝑊 ‘ 𝐵 ) ) } ) ⊆ 𝐵 )
41 4 40 eqsstrid ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝑂 –1-1→ 𝐴 ) → 𝐶 ⊆ 𝐵 )
42 34 simpld ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝑂 –1-1→ 𝐴 ) → 𝐵 ⊆ 𝐴 )
43 41 42 sstrd ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝑂 –1-1→ 𝐴 ) → 𝐶 ⊆ 𝐴 )
44 inss2 ⊢ ( ( 𝑊 ‘ 𝐵 ) ∩ ( 𝐶 × 𝐶 ) ) ⊆ ( 𝐶 × 𝐶 )
45 44 a1i ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝑂 –1-1→ 𝐴 ) → ( ( 𝑊 ‘ 𝐵 ) ∩ ( 𝐶 × 𝐶 ) ) ⊆ ( 𝐶 × 𝐶 ) )
46 33 simprd ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝑂 –1-1→ 𝐴 ) → ( ( 𝑊 ‘ 𝐵 ) We 𝐵 ∧ ∀ 𝑦 ∈ 𝐵 [ ( ◡ ( 𝑊 ‘ 𝐵 ) “ { 𝑦 } ) / 𝑢 ] ( 𝑢 𝐹 ( ( 𝑊 ‘ 𝐵 ) ∩ ( 𝑢 × 𝑢 ) ) ) = 𝑦 ) )
47 46 simpld ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝑂 –1-1→ 𝐴 ) → ( 𝑊 ‘ 𝐵 ) We 𝐵 )
48 wess ⊢ ( 𝐶 ⊆ 𝐵 → ( ( 𝑊 ‘ 𝐵 ) We 𝐵 → ( 𝑊 ‘ 𝐵 ) We 𝐶 ) )
49 41 47 48 sylc ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝑂 –1-1→ 𝐴 ) → ( 𝑊 ‘ 𝐵 ) We 𝐶 )
50 weinxp ⊢ ( ( 𝑊 ‘ 𝐵 ) We 𝐶 ↔ ( ( 𝑊 ‘ 𝐵 ) ∩ ( 𝐶 × 𝐶 ) ) We 𝐶 )
51 49 50 sylib ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝑂 –1-1→ 𝐴 ) → ( ( 𝑊 ‘ 𝐵 ) ∩ ( 𝐶 × 𝐶 ) ) We 𝐶 )
52 fvex ⊢ ( 𝑊 ‘ 𝐵 ) ∈ V
53 52 cnvex ⊢ ◡ ( 𝑊 ‘ 𝐵 ) ∈ V
54 53 imaex ⊢ ( ◡ ( 𝑊 ‘ 𝐵 ) “ { ( 𝐵 𝐹 ( 𝑊 ‘ 𝐵 ) ) } ) ∈ V
55 4 54 eqeltri ⊢ 𝐶 ∈ V
56 52 inex1 ⊢ ( ( 𝑊 ‘ 𝐵 ) ∩ ( 𝐶 × 𝐶 ) ) ∈ V
57 simpl ⊢ ( ( 𝑥 = 𝐶 ∧ 𝑟 = ( ( 𝑊 ‘ 𝐵 ) ∩ ( 𝐶 × 𝐶 ) ) ) → 𝑥 = 𝐶 )
58 57 sseq1d ⊢ ( ( 𝑥 = 𝐶 ∧ 𝑟 = ( ( 𝑊 ‘ 𝐵 ) ∩ ( 𝐶 × 𝐶 ) ) ) → ( 𝑥 ⊆ 𝐴 ↔ 𝐶 ⊆ 𝐴 ) )
59 simpr ⊢ ( ( 𝑥 = 𝐶 ∧ 𝑟 = ( ( 𝑊 ‘ 𝐵 ) ∩ ( 𝐶 × 𝐶 ) ) ) → 𝑟 = ( ( 𝑊 ‘ 𝐵 ) ∩ ( 𝐶 × 𝐶 ) ) )
60 57 sqxpeqd ⊢ ( ( 𝑥 = 𝐶 ∧ 𝑟 = ( ( 𝑊 ‘ 𝐵 ) ∩ ( 𝐶 × 𝐶 ) ) ) → ( 𝑥 × 𝑥 ) = ( 𝐶 × 𝐶 ) )
61 59 60 sseq12d ⊢ ( ( 𝑥 = 𝐶 ∧ 𝑟 = ( ( 𝑊 ‘ 𝐵 ) ∩ ( 𝐶 × 𝐶 ) ) ) → ( 𝑟 ⊆ ( 𝑥 × 𝑥 ) ↔ ( ( 𝑊 ‘ 𝐵 ) ∩ ( 𝐶 × 𝐶 ) ) ⊆ ( 𝐶 × 𝐶 ) ) )
62 59 57 weeq12d ⊢ ( ( 𝑥 = 𝐶 ∧ 𝑟 = ( ( 𝑊 ‘ 𝐵 ) ∩ ( 𝐶 × 𝐶 ) ) ) → ( 𝑟 We 𝑥 ↔ ( ( 𝑊 ‘ 𝐵 ) ∩ ( 𝐶 × 𝐶 ) ) We 𝐶 ) )
63 58 61 62 3anbi123d ⊢ ( ( 𝑥 = 𝐶 ∧ 𝑟 = ( ( 𝑊 ‘ 𝐵 ) ∩ ( 𝐶 × 𝐶 ) ) ) → ( ( 𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ ( 𝑥 × 𝑥 ) ∧ 𝑟 We 𝑥 ) ↔ ( 𝐶 ⊆ 𝐴 ∧ ( ( 𝑊 ‘ 𝐵 ) ∩ ( 𝐶 × 𝐶 ) ) ⊆ ( 𝐶 × 𝐶 ) ∧ ( ( 𝑊 ‘ 𝐵 ) ∩ ( 𝐶 × 𝐶 ) ) We 𝐶 ) ) )
64 55 56 63 opelopaba ⊢ ( ⟨ 𝐶 , ( ( 𝑊 ‘ 𝐵 ) ∩ ( 𝐶 × 𝐶 ) ) ⟩ ∈ { ⟨ 𝑥 , 𝑟 ⟩ ∣ ( 𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ ( 𝑥 × 𝑥 ) ∧ 𝑟 We 𝑥 ) } ↔ ( 𝐶 ⊆ 𝐴 ∧ ( ( 𝑊 ‘ 𝐵 ) ∩ ( 𝐶 × 𝐶 ) ) ⊆ ( 𝐶 × 𝐶 ) ∧ ( ( 𝑊 ‘ 𝐵 ) ∩ ( 𝐶 × 𝐶 ) ) We 𝐶 ) )
65 43 45 51 64 syl3anbrc ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝑂 –1-1→ 𝐴 ) → ⟨ 𝐶 , ( ( 𝑊 ‘ 𝐵 ) ∩ ( 𝐶 × 𝐶 ) ) ⟩ ∈ { ⟨ 𝑥 , 𝑟 ⟩ ∣ ( 𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ ( 𝑥 × 𝑥 ) ∧ 𝑟 We 𝑥 ) } )
66 65 1 eleqtrrdi ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝑂 –1-1→ 𝐴 ) → ⟨ 𝐶 , ( ( 𝑊 ‘ 𝐵 ) ∩ ( 𝐶 × 𝐶 ) ) ⟩ ∈ 𝑂 )
67 8 42 ssexd ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝑂 –1-1→ 𝐴 ) → 𝐵 ∈ V )
68 52 a1i ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝑂 –1-1→ 𝐴 ) → ( 𝑊 ‘ 𝐵 ) ∈ V )
69 simpl ⊢ ( ( 𝑥 = 𝐵 ∧ 𝑟 = ( 𝑊 ‘ 𝐵 ) ) → 𝑥 = 𝐵 )
70 69 sseq1d ⊢ ( ( 𝑥 = 𝐵 ∧ 𝑟 = ( 𝑊 ‘ 𝐵 ) ) → ( 𝑥 ⊆ 𝐴 ↔ 𝐵 ⊆ 𝐴 ) )
71 simpr ⊢ ( ( 𝑥 = 𝐵 ∧ 𝑟 = ( 𝑊 ‘ 𝐵 ) ) → 𝑟 = ( 𝑊 ‘ 𝐵 ) )
72 69 sqxpeqd ⊢ ( ( 𝑥 = 𝐵 ∧ 𝑟 = ( 𝑊 ‘ 𝐵 ) ) → ( 𝑥 × 𝑥 ) = ( 𝐵 × 𝐵 ) )
73 71 72 sseq12d ⊢ ( ( 𝑥 = 𝐵 ∧ 𝑟 = ( 𝑊 ‘ 𝐵 ) ) → ( 𝑟 ⊆ ( 𝑥 × 𝑥 ) ↔ ( 𝑊 ‘ 𝐵 ) ⊆ ( 𝐵 × 𝐵 ) ) )
74 71 69 weeq12d ⊢ ( ( 𝑥 = 𝐵 ∧ 𝑟 = ( 𝑊 ‘ 𝐵 ) ) → ( 𝑟 We 𝑥 ↔ ( 𝑊 ‘ 𝐵 ) We 𝐵 ) )
75 70 73 74 3anbi123d ⊢ ( ( 𝑥 = 𝐵 ∧ 𝑟 = ( 𝑊 ‘ 𝐵 ) ) → ( ( 𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ ( 𝑥 × 𝑥 ) ∧ 𝑟 We 𝑥 ) ↔ ( 𝐵 ⊆ 𝐴 ∧ ( 𝑊 ‘ 𝐵 ) ⊆ ( 𝐵 × 𝐵 ) ∧ ( 𝑊 ‘ 𝐵 ) We 𝐵 ) ) )
76 75 opelopabga ⊢ ( ( 𝐵 ∈ V ∧ ( 𝑊 ‘ 𝐵 ) ∈ V ) → ( ⟨ 𝐵 , ( 𝑊 ‘ 𝐵 ) ⟩ ∈ { ⟨ 𝑥 , 𝑟 ⟩ ∣ ( 𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ ( 𝑥 × 𝑥 ) ∧ 𝑟 We 𝑥 ) } ↔ ( 𝐵 ⊆ 𝐴 ∧ ( 𝑊 ‘ 𝐵 ) ⊆ ( 𝐵 × 𝐵 ) ∧ ( 𝑊 ‘ 𝐵 ) We 𝐵 ) ) )
77 67 68 76 syl2anc ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝑂 –1-1→ 𝐴 ) → ( ⟨ 𝐵 , ( 𝑊 ‘ 𝐵 ) ⟩ ∈ { ⟨ 𝑥 , 𝑟 ⟩ ∣ ( 𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ ( 𝑥 × 𝑥 ) ∧ 𝑟 We 𝑥 ) } ↔ ( 𝐵 ⊆ 𝐴 ∧ ( 𝑊 ‘ 𝐵 ) ⊆ ( 𝐵 × 𝐵 ) ∧ ( 𝑊 ‘ 𝐵 ) We 𝐵 ) ) )
78 42 35 47 77 mpbir3and ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝑂 –1-1→ 𝐴 ) → ⟨ 𝐵 , ( 𝑊 ‘ 𝐵 ) ⟩ ∈ { ⟨ 𝑥 , 𝑟 ⟩ ∣ ( 𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ ( 𝑥 × 𝑥 ) ∧ 𝑟 We 𝑥 ) } )
79 78 1 eleqtrrdi ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝑂 –1-1→ 𝐴 ) → ⟨ 𝐵 , ( 𝑊 ‘ 𝐵 ) ⟩ ∈ 𝑂 )
80 f1fveq ⊢ ( ( 𝐹 : 𝑂 –1-1→ 𝐴 ∧ ( ⟨ 𝐶 , ( ( 𝑊 ‘ 𝐵 ) ∩ ( 𝐶 × 𝐶 ) ) ⟩ ∈ 𝑂 ∧ ⟨ 𝐵 , ( 𝑊 ‘ 𝐵 ) ⟩ ∈ 𝑂 ) ) → ( ( 𝐹 ‘ ⟨ 𝐶 , ( ( 𝑊 ‘ 𝐵 ) ∩ ( 𝐶 × 𝐶 ) ) ⟩ ) = ( 𝐹 ‘ ⟨ 𝐵 , ( 𝑊 ‘ 𝐵 ) ⟩ ) ↔ ⟨ 𝐶 , ( ( 𝑊 ‘ 𝐵 ) ∩ ( 𝐶 × 𝐶 ) ) ⟩ = ⟨ 𝐵 , ( 𝑊 ‘ 𝐵 ) ⟩ ) )
81 30 66 79 80 syl12anc ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝑂 –1-1→ 𝐴 ) → ( ( 𝐹 ‘ ⟨ 𝐶 , ( ( 𝑊 ‘ 𝐵 ) ∩ ( 𝐶 × 𝐶 ) ) ⟩ ) = ( 𝐹 ‘ ⟨ 𝐵 , ( 𝑊 ‘ 𝐵 ) ⟩ ) ↔ ⟨ 𝐶 , ( ( 𝑊 ‘ 𝐵 ) ∩ ( 𝐶 × 𝐶 ) ) ⟩ = ⟨ 𝐵 , ( 𝑊 ‘ 𝐵 ) ⟩ ) )
82 29 81 mpbid ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝑂 –1-1→ 𝐴 ) → ⟨ 𝐶 , ( ( 𝑊 ‘ 𝐵 ) ∩ ( 𝐶 × 𝐶 ) ) ⟩ = ⟨ 𝐵 , ( 𝑊 ‘ 𝐵 ) ⟩ )
83 55 56 opth1 ⊢ ( ⟨ 𝐶 , ( ( 𝑊 ‘ 𝐵 ) ∩ ( 𝐶 × 𝐶 ) ) ⟩ = ⟨ 𝐵 , ( 𝑊 ‘ 𝐵 ) ⟩ → 𝐶 = 𝐵 )
84 82 83 syl ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝑂 –1-1→ 𝐴 ) → 𝐶 = 𝐵 )
85 19 84 eleqtrrd ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝑂 –1-1→ 𝐴 ) → ( 𝐵 𝐹 ( 𝑊 ‘ 𝐵 ) ) ∈ 𝐶 )
86 85 4 eleqtrdi ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝑂 –1-1→ 𝐴 ) → ( 𝐵 𝐹 ( 𝑊 ‘ 𝐵 ) ) ∈ ( ◡ ( 𝑊 ‘ 𝐵 ) “ { ( 𝐵 𝐹 ( 𝑊 ‘ 𝐵 ) ) } ) )
87 ovex ⊢ ( 𝐵 𝐹 ( 𝑊 ‘ 𝐵 ) ) ∈ V
88 87 eliniseg ⊢ ( ( 𝐵 𝐹 ( 𝑊 ‘ 𝐵 ) ) ∈ 𝐵 → ( ( 𝐵 𝐹 ( 𝑊 ‘ 𝐵 ) ) ∈ ( ◡ ( 𝑊 ‘ 𝐵 ) “ { ( 𝐵 𝐹 ( 𝑊 ‘ 𝐵 ) ) } ) ↔ ( 𝐵 𝐹 ( 𝑊 ‘ 𝐵 ) ) ( 𝑊 ‘ 𝐵 ) ( 𝐵 𝐹 ( 𝑊 ‘ 𝐵 ) ) ) )
89 19 88 syl ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝑂 –1-1→ 𝐴 ) → ( ( 𝐵 𝐹 ( 𝑊 ‘ 𝐵 ) ) ∈ ( ◡ ( 𝑊 ‘ 𝐵 ) “ { ( 𝐵 𝐹 ( 𝑊 ‘ 𝐵 ) ) } ) ↔ ( 𝐵 𝐹 ( 𝑊 ‘ 𝐵 ) ) ( 𝑊 ‘ 𝐵 ) ( 𝐵 𝐹 ( 𝑊 ‘ 𝐵 ) ) ) )
90 86 89 mpbid ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝑂 –1-1→ 𝐴 ) → ( 𝐵 𝐹 ( 𝑊 ‘ 𝐵 ) ) ( 𝑊 ‘ 𝐵 ) ( 𝐵 𝐹 ( 𝑊 ‘ 𝐵 ) ) )
91 weso ⊢ ( ( 𝑊 ‘ 𝐵 ) We 𝐵 → ( 𝑊 ‘ 𝐵 ) Or 𝐵 )
92 47 91 syl ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝑂 –1-1→ 𝐴 ) → ( 𝑊 ‘ 𝐵 ) Or 𝐵 )
93 sonr ⊢ ( ( ( 𝑊 ‘ 𝐵 ) Or 𝐵 ∧ ( 𝐵 𝐹 ( 𝑊 ‘ 𝐵 ) ) ∈ 𝐵 ) → ¬ ( 𝐵 𝐹 ( 𝑊 ‘ 𝐵 ) ) ( 𝑊 ‘ 𝐵 ) ( 𝐵 𝐹 ( 𝑊 ‘ 𝐵 ) ) )
94 92 19 93 syl2anc ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝑂 –1-1→ 𝐴 ) → ¬ ( 𝐵 𝐹 ( 𝑊 ‘ 𝐵 ) ) ( 𝑊 ‘ 𝐵 ) ( 𝐵 𝐹 ( 𝑊 ‘ 𝐵 ) ) )
95 90 94 pm2.65da ⊢ ( 𝐴 ∈ 𝑉 → ¬ 𝐹 : 𝑂 –1-1→ 𝐴 )