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