Metamath Proof Explorer

Theorem txsconnlem

Description: Lemma for txsconn . (Contributed by Mario Carneiro, 9-Mar-2015)

Ref Expression
Hypotheses txsconn.1 ⊢ ( 𝜑 → 𝑅 ∈ Top )
txsconn.2 ⊢ ( 𝜑 → 𝑆 ∈ Top )
txsconn.3 ⊢ ( 𝜑 → 𝐹 ∈ ( II Cn ( 𝑅 ×t 𝑆 ) ) )
txsconn.5 ⊢ 𝐴 = ( ( 1st ↾ ( ∪ 𝑅 × ∪ 𝑆 ) ) ∘ 𝐹 )
txsconn.6 ⊢ 𝐵 = ( ( 2nd ↾ ( ∪ 𝑅 × ∪ 𝑆 ) ) ∘ 𝐹 )
txsconn.7 ⊢ ( 𝜑 → 𝐺 ∈ ( 𝐴 ( PHtpy ‘ 𝑅 ) ( ( 0 [,] 1 ) × { ( 𝐴 ‘ 0 ) } ) ) )
txsconn.8 ⊢ ( 𝜑 → 𝐻 ∈ ( 𝐵 ( PHtpy ‘ 𝑆 ) ( ( 0 [,] 1 ) × { ( 𝐵 ‘ 0 ) } ) ) )
Assertion txsconnlem ( 𝜑 → 𝐹 ( ≃ph ‘ ( 𝑅 ×t 𝑆 ) ) ( ( 0 [,] 1 ) × { ( 𝐹 ‘ 0 ) } ) )

Proof

Step Hyp Ref Expression
1 txsconn.1 ⊢ ( 𝜑 → 𝑅 ∈ Top )
2 txsconn.2 ⊢ ( 𝜑 → 𝑆 ∈ Top )
3 txsconn.3 ⊢ ( 𝜑 → 𝐹 ∈ ( II Cn ( 𝑅 ×t 𝑆 ) ) )
4 txsconn.5 ⊢ 𝐴 = ( ( 1st ↾ ( ∪ 𝑅 × ∪ 𝑆 ) ) ∘ 𝐹 )
5 txsconn.6 ⊢ 𝐵 = ( ( 2nd ↾ ( ∪ 𝑅 × ∪ 𝑆 ) ) ∘ 𝐹 )
6 txsconn.7 ⊢ ( 𝜑 → 𝐺 ∈ ( 𝐴 ( PHtpy ‘ 𝑅 ) ( ( 0 [,] 1 ) × { ( 𝐴 ‘ 0 ) } ) ) )
7 txsconn.8 ⊢ ( 𝜑 → 𝐻 ∈ ( 𝐵 ( PHtpy ‘ 𝑆 ) ( ( 0 [,] 1 ) × { ( 𝐵 ‘ 0 ) } ) ) )
8 fconstmpt ⊢ ( ( 0 [,] 1 ) × { ( 𝐹 ‘ 0 ) } ) = ( 𝑥 ∈ ( 0 [,] 1 ) ↦ ( 𝐹 ‘ 0 ) )
9 iitopon ⊢ II ∈ ( TopOn ‘ ( 0 [,] 1 ) )
10 9 a1i ⊢ ( 𝜑 → II ∈ ( TopOn ‘ ( 0 [,] 1 ) ) )
11 eqid ⊢ ∪ 𝑅 = ∪ 𝑅
12 11 toptopon ⊢ ( 𝑅 ∈ Top ↔ 𝑅 ∈ ( TopOn ‘ ∪ 𝑅 ) )
13 1 12 sylib ⊢ ( 𝜑 → 𝑅 ∈ ( TopOn ‘ ∪ 𝑅 ) )
14 eqid ⊢ ∪ 𝑆 = ∪ 𝑆
15 14 toptopon ⊢ ( 𝑆 ∈ Top ↔ 𝑆 ∈ ( TopOn ‘ ∪ 𝑆 ) )
16 2 15 sylib ⊢ ( 𝜑 → 𝑆 ∈ ( TopOn ‘ ∪ 𝑆 ) )
17 txtopon ⊢ ( ( 𝑅 ∈ ( TopOn ‘ ∪ 𝑅 ) ∧ 𝑆 ∈ ( TopOn ‘ ∪ 𝑆 ) ) → ( 𝑅 ×t 𝑆 ) ∈ ( TopOn ‘ ( ∪ 𝑅 × ∪ 𝑆 ) ) )
18 13 16 17 syl2anc ⊢ ( 𝜑 → ( 𝑅 ×t 𝑆 ) ∈ ( TopOn ‘ ( ∪ 𝑅 × ∪ 𝑆 ) ) )
19 cnf2 ⊢ ( ( II ∈ ( TopOn ‘ ( 0 [,] 1 ) ) ∧ ( 𝑅 ×t 𝑆 ) ∈ ( TopOn ‘ ( ∪ 𝑅 × ∪ 𝑆 ) ) ∧ 𝐹 ∈ ( II Cn ( 𝑅 ×t 𝑆 ) ) ) → 𝐹 : ( 0 [,] 1 ) ⟶ ( ∪ 𝑅 × ∪ 𝑆 ) )
20 10 18 3 19 syl3anc ⊢ ( 𝜑 → 𝐹 : ( 0 [,] 1 ) ⟶ ( ∪ 𝑅 × ∪ 𝑆 ) )
21 0elunit ⊢ 0 ∈ ( 0 [,] 1 )
22 ffvelrn ⊢ ( ( 𝐹 : ( 0 [,] 1 ) ⟶ ( ∪ 𝑅 × ∪ 𝑆 ) ∧ 0 ∈ ( 0 [,] 1 ) ) → ( 𝐹 ‘ 0 ) ∈ ( ∪ 𝑅 × ∪ 𝑆 ) )
23 20 21 22 sylancl ⊢ ( 𝜑 → ( 𝐹 ‘ 0 ) ∈ ( ∪ 𝑅 × ∪ 𝑆 ) )
24 10 18 23 cnmptc ⊢ ( 𝜑 → ( 𝑥 ∈ ( 0 [,] 1 ) ↦ ( 𝐹 ‘ 0 ) ) ∈ ( II Cn ( 𝑅 ×t 𝑆 ) ) )
25 8 24 eqeltrid ⊢ ( 𝜑 → ( ( 0 [,] 1 ) × { ( 𝐹 ‘ 0 ) } ) ∈ ( II Cn ( 𝑅 ×t 𝑆 ) ) )
26 tx1cn ⊢ ( ( 𝑅 ∈ ( TopOn ‘ ∪ 𝑅 ) ∧ 𝑆 ∈ ( TopOn ‘ ∪ 𝑆 ) ) → ( 1st ↾ ( ∪ 𝑅 × ∪ 𝑆 ) ) ∈ ( ( 𝑅 ×t 𝑆 ) Cn 𝑅 ) )
27 13 16 26 syl2anc ⊢ ( 𝜑 → ( 1st ↾ ( ∪ 𝑅 × ∪ 𝑆 ) ) ∈ ( ( 𝑅 ×t 𝑆 ) Cn 𝑅 ) )
28 cnco ⊢ ( ( 𝐹 ∈ ( II Cn ( 𝑅 ×t 𝑆 ) ) ∧ ( 1st ↾ ( ∪ 𝑅 × ∪ 𝑆 ) ) ∈ ( ( 𝑅 ×t 𝑆 ) Cn 𝑅 ) ) → ( ( 1st ↾ ( ∪ 𝑅 × ∪ 𝑆 ) ) ∘ 𝐹 ) ∈ ( II Cn 𝑅 ) )
29 3 27 28 syl2anc ⊢ ( 𝜑 → ( ( 1st ↾ ( ∪ 𝑅 × ∪ 𝑆 ) ) ∘ 𝐹 ) ∈ ( II Cn 𝑅 ) )
30 4 29 eqeltrid ⊢ ( 𝜑 → 𝐴 ∈ ( II Cn 𝑅 ) )
31 fconstmpt ⊢ ( ( 0 [,] 1 ) × { ( 𝐴 ‘ 0 ) } ) = ( 𝑥 ∈ ( 0 [,] 1 ) ↦ ( 𝐴 ‘ 0 ) )
32 iiuni ⊢ ( 0 [,] 1 ) = ∪ II
33 32 11 cnf ⊢ ( 𝐴 ∈ ( II Cn 𝑅 ) → 𝐴 : ( 0 [,] 1 ) ⟶ ∪ 𝑅 )
34 30 33 syl ⊢ ( 𝜑 → 𝐴 : ( 0 [,] 1 ) ⟶ ∪ 𝑅 )
35 ffvelrn ⊢ ( ( 𝐴 : ( 0 [,] 1 ) ⟶ ∪ 𝑅 ∧ 0 ∈ ( 0 [,] 1 ) ) → ( 𝐴 ‘ 0 ) ∈ ∪ 𝑅 )
36 34 21 35 sylancl ⊢ ( 𝜑 → ( 𝐴 ‘ 0 ) ∈ ∪ 𝑅 )
37 10 13 36 cnmptc ⊢ ( 𝜑 → ( 𝑥 ∈ ( 0 [,] 1 ) ↦ ( 𝐴 ‘ 0 ) ) ∈ ( II Cn 𝑅 ) )
38 31 37 eqeltrid ⊢ ( 𝜑 → ( ( 0 [,] 1 ) × { ( 𝐴 ‘ 0 ) } ) ∈ ( II Cn 𝑅 ) )
39 30 38 phtpycn ⊢ ( 𝜑 → ( 𝐴 ( PHtpy ‘ 𝑅 ) ( ( 0 [,] 1 ) × { ( 𝐴 ‘ 0 ) } ) ) ⊆ ( ( II ×t II ) Cn 𝑅 ) )
40 39 6 sseldd ⊢ ( 𝜑 → 𝐺 ∈ ( ( II ×t II ) Cn 𝑅 ) )
41 iitop ⊢ II ∈ Top
42 41 41 32 32 txunii ⊢ ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) = ∪ ( II ×t II )
43 42 11 cnf ⊢ ( 𝐺 ∈ ( ( II ×t II ) Cn 𝑅 ) → 𝐺 : ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) ⟶ ∪ 𝑅 )
44 ffn ⊢ ( 𝐺 : ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) ⟶ ∪ 𝑅 → 𝐺 Fn ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) )
45 40 43 44 3syl ⊢ ( 𝜑 → 𝐺 Fn ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) )
46 fnov ⊢ ( 𝐺 Fn ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) ↔ 𝐺 = ( 𝑥 ∈ ( 0 [,] 1 ) , 𝑦 ∈ ( 0 [,] 1 ) ↦ ( 𝑥 𝐺 𝑦 ) ) )
47 45 46 sylib ⊢ ( 𝜑 → 𝐺 = ( 𝑥 ∈ ( 0 [,] 1 ) , 𝑦 ∈ ( 0 [,] 1 ) ↦ ( 𝑥 𝐺 𝑦 ) ) )
48 47 40 eqeltrrd ⊢ ( 𝜑 → ( 𝑥 ∈ ( 0 [,] 1 ) , 𝑦 ∈ ( 0 [,] 1 ) ↦ ( 𝑥 𝐺 𝑦 ) ) ∈ ( ( II ×t II ) Cn 𝑅 ) )
49 tx2cn ⊢ ( ( 𝑅 ∈ ( TopOn ‘ ∪ 𝑅 ) ∧ 𝑆 ∈ ( TopOn ‘ ∪ 𝑆 ) ) → ( 2nd ↾ ( ∪ 𝑅 × ∪ 𝑆 ) ) ∈ ( ( 𝑅 ×t 𝑆 ) Cn 𝑆 ) )
50 13 16 49 syl2anc ⊢ ( 𝜑 → ( 2nd ↾ ( ∪ 𝑅 × ∪ 𝑆 ) ) ∈ ( ( 𝑅 ×t 𝑆 ) Cn 𝑆 ) )
51 cnco ⊢ ( ( 𝐹 ∈ ( II Cn ( 𝑅 ×t 𝑆 ) ) ∧ ( 2nd ↾ ( ∪ 𝑅 × ∪ 𝑆 ) ) ∈ ( ( 𝑅 ×t 𝑆 ) Cn 𝑆 ) ) → ( ( 2nd ↾ ( ∪ 𝑅 × ∪ 𝑆 ) ) ∘ 𝐹 ) ∈ ( II Cn 𝑆 ) )
52 3 50 51 syl2anc ⊢ ( 𝜑 → ( ( 2nd ↾ ( ∪ 𝑅 × ∪ 𝑆 ) ) ∘ 𝐹 ) ∈ ( II Cn 𝑆 ) )
53 5 52 eqeltrid ⊢ ( 𝜑 → 𝐵 ∈ ( II Cn 𝑆 ) )
54 fconstmpt ⊢ ( ( 0 [,] 1 ) × { ( 𝐵 ‘ 0 ) } ) = ( 𝑥 ∈ ( 0 [,] 1 ) ↦ ( 𝐵 ‘ 0 ) )
55 32 14 cnf ⊢ ( 𝐵 ∈ ( II Cn 𝑆 ) → 𝐵 : ( 0 [,] 1 ) ⟶ ∪ 𝑆 )
56 53 55 syl ⊢ ( 𝜑 → 𝐵 : ( 0 [,] 1 ) ⟶ ∪ 𝑆 )
57 ffvelrn ⊢ ( ( 𝐵 : ( 0 [,] 1 ) ⟶ ∪ 𝑆 ∧ 0 ∈ ( 0 [,] 1 ) ) → ( 𝐵 ‘ 0 ) ∈ ∪ 𝑆 )
58 56 21 57 sylancl ⊢ ( 𝜑 → ( 𝐵 ‘ 0 ) ∈ ∪ 𝑆 )
59 10 16 58 cnmptc ⊢ ( 𝜑 → ( 𝑥 ∈ ( 0 [,] 1 ) ↦ ( 𝐵 ‘ 0 ) ) ∈ ( II Cn 𝑆 ) )
60 54 59 eqeltrid ⊢ ( 𝜑 → ( ( 0 [,] 1 ) × { ( 𝐵 ‘ 0 ) } ) ∈ ( II Cn 𝑆 ) )
61 53 60 phtpycn ⊢ ( 𝜑 → ( 𝐵 ( PHtpy ‘ 𝑆 ) ( ( 0 [,] 1 ) × { ( 𝐵 ‘ 0 ) } ) ) ⊆ ( ( II ×t II ) Cn 𝑆 ) )
62 61 7 sseldd ⊢ ( 𝜑 → 𝐻 ∈ ( ( II ×t II ) Cn 𝑆 ) )
63 42 14 cnf ⊢ ( 𝐻 ∈ ( ( II ×t II ) Cn 𝑆 ) → 𝐻 : ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) ⟶ ∪ 𝑆 )
64 ffn ⊢ ( 𝐻 : ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) ⟶ ∪ 𝑆 → 𝐻 Fn ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) )
65 62 63 64 3syl ⊢ ( 𝜑 → 𝐻 Fn ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) )
66 fnov ⊢ ( 𝐻 Fn ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) ↔ 𝐻 = ( 𝑥 ∈ ( 0 [,] 1 ) , 𝑦 ∈ ( 0 [,] 1 ) ↦ ( 𝑥 𝐻 𝑦 ) ) )
67 65 66 sylib ⊢ ( 𝜑 → 𝐻 = ( 𝑥 ∈ ( 0 [,] 1 ) , 𝑦 ∈ ( 0 [,] 1 ) ↦ ( 𝑥 𝐻 𝑦 ) ) )
68 67 62 eqeltrrd ⊢ ( 𝜑 → ( 𝑥 ∈ ( 0 [,] 1 ) , 𝑦 ∈ ( 0 [,] 1 ) ↦ ( 𝑥 𝐻 𝑦 ) ) ∈ ( ( II ×t II ) Cn 𝑆 ) )
69 10 10 48 68 cnmpt2t ⊢ ( 𝜑 → ( 𝑥 ∈ ( 0 [,] 1 ) , 𝑦 ∈ ( 0 [,] 1 ) ↦ ⟨ ( 𝑥 𝐺 𝑦 ) , ( 𝑥 𝐻 𝑦 ) ⟩ ) ∈ ( ( II ×t II ) Cn ( 𝑅 ×t 𝑆 ) ) )
70 30 38 phtpyhtpy ⊢ ( 𝜑 → ( 𝐴 ( PHtpy ‘ 𝑅 ) ( ( 0 [,] 1 ) × { ( 𝐴 ‘ 0 ) } ) ) ⊆ ( 𝐴 ( II Htpy 𝑅 ) ( ( 0 [,] 1 ) × { ( 𝐴 ‘ 0 ) } ) ) )
71 70 6 sseldd ⊢ ( 𝜑 → 𝐺 ∈ ( 𝐴 ( II Htpy 𝑅 ) ( ( 0 [,] 1 ) × { ( 𝐴 ‘ 0 ) } ) ) )
72 10 30 38 71 htpyi ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 0 [,] 1 ) ) → ( ( 𝑠 𝐺 0 ) = ( 𝐴 ‘ 𝑠 ) ∧ ( 𝑠 𝐺 1 ) = ( ( ( 0 [,] 1 ) × { ( 𝐴 ‘ 0 ) } ) ‘ 𝑠 ) ) )
73 72 simpld ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 0 [,] 1 ) ) → ( 𝑠 𝐺 0 ) = ( 𝐴 ‘ 𝑠 ) )
74 4 fveq1i ⊢ ( 𝐴 ‘ 𝑠 ) = ( ( ( 1st ↾ ( ∪ 𝑅 × ∪ 𝑆 ) ) ∘ 𝐹 ) ‘ 𝑠 )
75 fvco3 ⊢ ( ( 𝐹 : ( 0 [,] 1 ) ⟶ ( ∪ 𝑅 × ∪ 𝑆 ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) → ( ( ( 1st ↾ ( ∪ 𝑅 × ∪ 𝑆 ) ) ∘ 𝐹 ) ‘ 𝑠 ) = ( ( 1st ↾ ( ∪ 𝑅 × ∪ 𝑆 ) ) ‘ ( 𝐹 ‘ 𝑠 ) ) )
76 20 75 sylan ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 0 [,] 1 ) ) → ( ( ( 1st ↾ ( ∪ 𝑅 × ∪ 𝑆 ) ) ∘ 𝐹 ) ‘ 𝑠 ) = ( ( 1st ↾ ( ∪ 𝑅 × ∪ 𝑆 ) ) ‘ ( 𝐹 ‘ 𝑠 ) ) )
77 74 76 syl5eq ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 0 [,] 1 ) ) → ( 𝐴 ‘ 𝑠 ) = ( ( 1st ↾ ( ∪ 𝑅 × ∪ 𝑆 ) ) ‘ ( 𝐹 ‘ 𝑠 ) ) )
78 ffvelrn ⊢ ( ( 𝐹 : ( 0 [,] 1 ) ⟶ ( ∪ 𝑅 × ∪ 𝑆 ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) → ( 𝐹 ‘ 𝑠 ) ∈ ( ∪ 𝑅 × ∪ 𝑆 ) )
79 20 78 sylan ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 0 [,] 1 ) ) → ( 𝐹 ‘ 𝑠 ) ∈ ( ∪ 𝑅 × ∪ 𝑆 ) )
80 fvres ⊢ ( ( 𝐹 ‘ 𝑠 ) ∈ ( ∪ 𝑅 × ∪ 𝑆 ) → ( ( 1st ↾ ( ∪ 𝑅 × ∪ 𝑆 ) ) ‘ ( 𝐹 ‘ 𝑠 ) ) = ( 1st ‘ ( 𝐹 ‘ 𝑠 ) ) )
81 79 80 syl ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 0 [,] 1 ) ) → ( ( 1st ↾ ( ∪ 𝑅 × ∪ 𝑆 ) ) ‘ ( 𝐹 ‘ 𝑠 ) ) = ( 1st ‘ ( 𝐹 ‘ 𝑠 ) ) )
82 73 77 81 3eqtrd ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 0 [,] 1 ) ) → ( 𝑠 𝐺 0 ) = ( 1st ‘ ( 𝐹 ‘ 𝑠 ) ) )
83 53 60 phtpyhtpy ⊢ ( 𝜑 → ( 𝐵 ( PHtpy ‘ 𝑆 ) ( ( 0 [,] 1 ) × { ( 𝐵 ‘ 0 ) } ) ) ⊆ ( 𝐵 ( II Htpy 𝑆 ) ( ( 0 [,] 1 ) × { ( 𝐵 ‘ 0 ) } ) ) )
84 83 7 sseldd ⊢ ( 𝜑 → 𝐻 ∈ ( 𝐵 ( II Htpy 𝑆 ) ( ( 0 [,] 1 ) × { ( 𝐵 ‘ 0 ) } ) ) )
85 10 53 60 84 htpyi ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 0 [,] 1 ) ) → ( ( 𝑠 𝐻 0 ) = ( 𝐵 ‘ 𝑠 ) ∧ ( 𝑠 𝐻 1 ) = ( ( ( 0 [,] 1 ) × { ( 𝐵 ‘ 0 ) } ) ‘ 𝑠 ) ) )
86 85 simpld ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 0 [,] 1 ) ) → ( 𝑠 𝐻 0 ) = ( 𝐵 ‘ 𝑠 ) )
87 5 fveq1i ⊢ ( 𝐵 ‘ 𝑠 ) = ( ( ( 2nd ↾ ( ∪ 𝑅 × ∪ 𝑆 ) ) ∘ 𝐹 ) ‘ 𝑠 )
88 fvco3 ⊢ ( ( 𝐹 : ( 0 [,] 1 ) ⟶ ( ∪ 𝑅 × ∪ 𝑆 ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) → ( ( ( 2nd ↾ ( ∪ 𝑅 × ∪ 𝑆 ) ) ∘ 𝐹 ) ‘ 𝑠 ) = ( ( 2nd ↾ ( ∪ 𝑅 × ∪ 𝑆 ) ) ‘ ( 𝐹 ‘ 𝑠 ) ) )
89 20 88 sylan ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 0 [,] 1 ) ) → ( ( ( 2nd ↾ ( ∪ 𝑅 × ∪ 𝑆 ) ) ∘ 𝐹 ) ‘ 𝑠 ) = ( ( 2nd ↾ ( ∪ 𝑅 × ∪ 𝑆 ) ) ‘ ( 𝐹 ‘ 𝑠 ) ) )
90 87 89 syl5eq ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 0 [,] 1 ) ) → ( 𝐵 ‘ 𝑠 ) = ( ( 2nd ↾ ( ∪ 𝑅 × ∪ 𝑆 ) ) ‘ ( 𝐹 ‘ 𝑠 ) ) )
91 fvres ⊢ ( ( 𝐹 ‘ 𝑠 ) ∈ ( ∪ 𝑅 × ∪ 𝑆 ) → ( ( 2nd ↾ ( ∪ 𝑅 × ∪ 𝑆 ) ) ‘ ( 𝐹 ‘ 𝑠 ) ) = ( 2nd ‘ ( 𝐹 ‘ 𝑠 ) ) )
92 79 91 syl ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 0 [,] 1 ) ) → ( ( 2nd ↾ ( ∪ 𝑅 × ∪ 𝑆 ) ) ‘ ( 𝐹 ‘ 𝑠 ) ) = ( 2nd ‘ ( 𝐹 ‘ 𝑠 ) ) )
93 86 90 92 3eqtrd ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 0 [,] 1 ) ) → ( 𝑠 𝐻 0 ) = ( 2nd ‘ ( 𝐹 ‘ 𝑠 ) ) )
94 82 93 opeq12d ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 0 [,] 1 ) ) → ⟨ ( 𝑠 𝐺 0 ) , ( 𝑠 𝐻 0 ) ⟩ = ⟨ ( 1st ‘ ( 𝐹 ‘ 𝑠 ) ) , ( 2nd ‘ ( 𝐹 ‘ 𝑠 ) ) ⟩ )
95 simpr ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 0 [,] 1 ) ) → 𝑠 ∈ ( 0 [,] 1 ) )
96 oveq12 ⊢ ( ( 𝑥 = 𝑠 ∧ 𝑦 = 0 ) → ( 𝑥 𝐺 𝑦 ) = ( 𝑠 𝐺 0 ) )
97 oveq12 ⊢ ( ( 𝑥 = 𝑠 ∧ 𝑦 = 0 ) → ( 𝑥 𝐻 𝑦 ) = ( 𝑠 𝐻 0 ) )
98 96 97 opeq12d ⊢ ( ( 𝑥 = 𝑠 ∧ 𝑦 = 0 ) → ⟨ ( 𝑥 𝐺 𝑦 ) , ( 𝑥 𝐻 𝑦 ) ⟩ = ⟨ ( 𝑠 𝐺 0 ) , ( 𝑠 𝐻 0 ) ⟩ )
99 eqid ⊢ ( 𝑥 ∈ ( 0 [,] 1 ) , 𝑦 ∈ ( 0 [,] 1 ) ↦ ⟨ ( 𝑥 𝐺 𝑦 ) , ( 𝑥 𝐻 𝑦 ) ⟩ ) = ( 𝑥 ∈ ( 0 [,] 1 ) , 𝑦 ∈ ( 0 [,] 1 ) ↦ ⟨ ( 𝑥 𝐺 𝑦 ) , ( 𝑥 𝐻 𝑦 ) ⟩ )
100 opex ⊢ ⟨ ( 𝑠 𝐺 0 ) , ( 𝑠 𝐻 0 ) ⟩ ∈ V
101 98 99 100 ovmpoa ⊢ ( ( 𝑠 ∈ ( 0 [,] 1 ) ∧ 0 ∈ ( 0 [,] 1 ) ) → ( 𝑠 ( 𝑥 ∈ ( 0 [,] 1 ) , 𝑦 ∈ ( 0 [,] 1 ) ↦ ⟨ ( 𝑥 𝐺 𝑦 ) , ( 𝑥 𝐻 𝑦 ) ⟩ ) 0 ) = ⟨ ( 𝑠 𝐺 0 ) , ( 𝑠 𝐻 0 ) ⟩ )
102 95 21 101 sylancl ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 0 [,] 1 ) ) → ( 𝑠 ( 𝑥 ∈ ( 0 [,] 1 ) , 𝑦 ∈ ( 0 [,] 1 ) ↦ ⟨ ( 𝑥 𝐺 𝑦 ) , ( 𝑥 𝐻 𝑦 ) ⟩ ) 0 ) = ⟨ ( 𝑠 𝐺 0 ) , ( 𝑠 𝐻 0 ) ⟩ )
103 1st2nd2 ⊢ ( ( 𝐹 ‘ 𝑠 ) ∈ ( ∪ 𝑅 × ∪ 𝑆 ) → ( 𝐹 ‘ 𝑠 ) = ⟨ ( 1st ‘ ( 𝐹 ‘ 𝑠 ) ) , ( 2nd ‘ ( 𝐹 ‘ 𝑠 ) ) ⟩ )
104 79 103 syl ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 0 [,] 1 ) ) → ( 𝐹 ‘ 𝑠 ) = ⟨ ( 1st ‘ ( 𝐹 ‘ 𝑠 ) ) , ( 2nd ‘ ( 𝐹 ‘ 𝑠 ) ) ⟩ )
105 94 102 104 3eqtr4d ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 0 [,] 1 ) ) → ( 𝑠 ( 𝑥 ∈ ( 0 [,] 1 ) , 𝑦 ∈ ( 0 [,] 1 ) ↦ ⟨ ( 𝑥 𝐺 𝑦 ) , ( 𝑥 𝐻 𝑦 ) ⟩ ) 0 ) = ( 𝐹 ‘ 𝑠 ) )
106 72 simprd ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 0 [,] 1 ) ) → ( 𝑠 𝐺 1 ) = ( ( ( 0 [,] 1 ) × { ( 𝐴 ‘ 0 ) } ) ‘ 𝑠 ) )
107 fvex ⊢ ( 𝐴 ‘ 0 ) ∈ V
108 107 fvconst2 ⊢ ( 𝑠 ∈ ( 0 [,] 1 ) → ( ( ( 0 [,] 1 ) × { ( 𝐴 ‘ 0 ) } ) ‘ 𝑠 ) = ( 𝐴 ‘ 0 ) )
109 108 adantl ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 0 [,] 1 ) ) → ( ( ( 0 [,] 1 ) × { ( 𝐴 ‘ 0 ) } ) ‘ 𝑠 ) = ( 𝐴 ‘ 0 ) )
110 4 fveq1i ⊢ ( 𝐴 ‘ 0 ) = ( ( ( 1st ↾ ( ∪ 𝑅 × ∪ 𝑆 ) ) ∘ 𝐹 ) ‘ 0 )
111 fvco3 ⊢ ( ( 𝐹 : ( 0 [,] 1 ) ⟶ ( ∪ 𝑅 × ∪ 𝑆 ) ∧ 0 ∈ ( 0 [,] 1 ) ) → ( ( ( 1st ↾ ( ∪ 𝑅 × ∪ 𝑆 ) ) ∘ 𝐹 ) ‘ 0 ) = ( ( 1st ↾ ( ∪ 𝑅 × ∪ 𝑆 ) ) ‘ ( 𝐹 ‘ 0 ) ) )
112 20 21 111 sylancl ⊢ ( 𝜑 → ( ( ( 1st ↾ ( ∪ 𝑅 × ∪ 𝑆 ) ) ∘ 𝐹 ) ‘ 0 ) = ( ( 1st ↾ ( ∪ 𝑅 × ∪ 𝑆 ) ) ‘ ( 𝐹 ‘ 0 ) ) )
113 fvres ⊢ ( ( 𝐹 ‘ 0 ) ∈ ( ∪ 𝑅 × ∪ 𝑆 ) → ( ( 1st ↾ ( ∪ 𝑅 × ∪ 𝑆 ) ) ‘ ( 𝐹 ‘ 0 ) ) = ( 1st ‘ ( 𝐹 ‘ 0 ) ) )
114 23 113 syl ⊢ ( 𝜑 → ( ( 1st ↾ ( ∪ 𝑅 × ∪ 𝑆 ) ) ‘ ( 𝐹 ‘ 0 ) ) = ( 1st ‘ ( 𝐹 ‘ 0 ) ) )
115 112 114 eqtrd ⊢ ( 𝜑 → ( ( ( 1st ↾ ( ∪ 𝑅 × ∪ 𝑆 ) ) ∘ 𝐹 ) ‘ 0 ) = ( 1st ‘ ( 𝐹 ‘ 0 ) ) )
116 110 115 syl5eq ⊢ ( 𝜑 → ( 𝐴 ‘ 0 ) = ( 1st ‘ ( 𝐹 ‘ 0 ) ) )
117 116 adantr ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 0 [,] 1 ) ) → ( 𝐴 ‘ 0 ) = ( 1st ‘ ( 𝐹 ‘ 0 ) ) )
118 106 109 117 3eqtrd ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 0 [,] 1 ) ) → ( 𝑠 𝐺 1 ) = ( 1st ‘ ( 𝐹 ‘ 0 ) ) )
119 85 simprd ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 0 [,] 1 ) ) → ( 𝑠 𝐻 1 ) = ( ( ( 0 [,] 1 ) × { ( 𝐵 ‘ 0 ) } ) ‘ 𝑠 ) )
120 fvex ⊢ ( 𝐵 ‘ 0 ) ∈ V
121 120 fvconst2 ⊢ ( 𝑠 ∈ ( 0 [,] 1 ) → ( ( ( 0 [,] 1 ) × { ( 𝐵 ‘ 0 ) } ) ‘ 𝑠 ) = ( 𝐵 ‘ 0 ) )
122 121 adantl ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 0 [,] 1 ) ) → ( ( ( 0 [,] 1 ) × { ( 𝐵 ‘ 0 ) } ) ‘ 𝑠 ) = ( 𝐵 ‘ 0 ) )
123 5 fveq1i ⊢ ( 𝐵 ‘ 0 ) = ( ( ( 2nd ↾ ( ∪ 𝑅 × ∪ 𝑆 ) ) ∘ 𝐹 ) ‘ 0 )
124 fvco3 ⊢ ( ( 𝐹 : ( 0 [,] 1 ) ⟶ ( ∪ 𝑅 × ∪ 𝑆 ) ∧ 0 ∈ ( 0 [,] 1 ) ) → ( ( ( 2nd ↾ ( ∪ 𝑅 × ∪ 𝑆 ) ) ∘ 𝐹 ) ‘ 0 ) = ( ( 2nd ↾ ( ∪ 𝑅 × ∪ 𝑆 ) ) ‘ ( 𝐹 ‘ 0 ) ) )
125 20 21 124 sylancl ⊢ ( 𝜑 → ( ( ( 2nd ↾ ( ∪ 𝑅 × ∪ 𝑆 ) ) ∘ 𝐹 ) ‘ 0 ) = ( ( 2nd ↾ ( ∪ 𝑅 × ∪ 𝑆 ) ) ‘ ( 𝐹 ‘ 0 ) ) )
126 fvres ⊢ ( ( 𝐹 ‘ 0 ) ∈ ( ∪ 𝑅 × ∪ 𝑆 ) → ( ( 2nd ↾ ( ∪ 𝑅 × ∪ 𝑆 ) ) ‘ ( 𝐹 ‘ 0 ) ) = ( 2nd ‘ ( 𝐹 ‘ 0 ) ) )
127 23 126 syl ⊢ ( 𝜑 → ( ( 2nd ↾ ( ∪ 𝑅 × ∪ 𝑆 ) ) ‘ ( 𝐹 ‘ 0 ) ) = ( 2nd ‘ ( 𝐹 ‘ 0 ) ) )
128 125 127 eqtrd ⊢ ( 𝜑 → ( ( ( 2nd ↾ ( ∪ 𝑅 × ∪ 𝑆 ) ) ∘ 𝐹 ) ‘ 0 ) = ( 2nd ‘ ( 𝐹 ‘ 0 ) ) )
129 123 128 syl5eq ⊢ ( 𝜑 → ( 𝐵 ‘ 0 ) = ( 2nd ‘ ( 𝐹 ‘ 0 ) ) )
130 129 adantr ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 0 [,] 1 ) ) → ( 𝐵 ‘ 0 ) = ( 2nd ‘ ( 𝐹 ‘ 0 ) ) )
131 119 122 130 3eqtrd ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 0 [,] 1 ) ) → ( 𝑠 𝐻 1 ) = ( 2nd ‘ ( 𝐹 ‘ 0 ) ) )
132 118 131 opeq12d ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 0 [,] 1 ) ) → ⟨ ( 𝑠 𝐺 1 ) , ( 𝑠 𝐻 1 ) ⟩ = ⟨ ( 1st ‘ ( 𝐹 ‘ 0 ) ) , ( 2nd ‘ ( 𝐹 ‘ 0 ) ) ⟩ )
133 1elunit ⊢ 1 ∈ ( 0 [,] 1 )
134 oveq12 ⊢ ( ( 𝑥 = 𝑠 ∧ 𝑦 = 1 ) → ( 𝑥 𝐺 𝑦 ) = ( 𝑠 𝐺 1 ) )
135 oveq12 ⊢ ( ( 𝑥 = 𝑠 ∧ 𝑦 = 1 ) → ( 𝑥 𝐻 𝑦 ) = ( 𝑠 𝐻 1 ) )
136 134 135 opeq12d ⊢ ( ( 𝑥 = 𝑠 ∧ 𝑦 = 1 ) → ⟨ ( 𝑥 𝐺 𝑦 ) , ( 𝑥 𝐻 𝑦 ) ⟩ = ⟨ ( 𝑠 𝐺 1 ) , ( 𝑠 𝐻 1 ) ⟩ )
137 opex ⊢ ⟨ ( 𝑠 𝐺 1 ) , ( 𝑠 𝐻 1 ) ⟩ ∈ V
138 136 99 137 ovmpoa ⊢ ( ( 𝑠 ∈ ( 0 [,] 1 ) ∧ 1 ∈ ( 0 [,] 1 ) ) → ( 𝑠 ( 𝑥 ∈ ( 0 [,] 1 ) , 𝑦 ∈ ( 0 [,] 1 ) ↦ ⟨ ( 𝑥 𝐺 𝑦 ) , ( 𝑥 𝐻 𝑦 ) ⟩ ) 1 ) = ⟨ ( 𝑠 𝐺 1 ) , ( 𝑠 𝐻 1 ) ⟩ )
139 95 133 138 sylancl ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 0 [,] 1 ) ) → ( 𝑠 ( 𝑥 ∈ ( 0 [,] 1 ) , 𝑦 ∈ ( 0 [,] 1 ) ↦ ⟨ ( 𝑥 𝐺 𝑦 ) , ( 𝑥 𝐻 𝑦 ) ⟩ ) 1 ) = ⟨ ( 𝑠 𝐺 1 ) , ( 𝑠 𝐻 1 ) ⟩ )
140 fvex ⊢ ( 𝐹 ‘ 0 ) ∈ V
141 140 fvconst2 ⊢ ( 𝑠 ∈ ( 0 [,] 1 ) → ( ( ( 0 [,] 1 ) × { ( 𝐹 ‘ 0 ) } ) ‘ 𝑠 ) = ( 𝐹 ‘ 0 ) )
142 141 adantl ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 0 [,] 1 ) ) → ( ( ( 0 [,] 1 ) × { ( 𝐹 ‘ 0 ) } ) ‘ 𝑠 ) = ( 𝐹 ‘ 0 ) )
143 23 adantr ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 0 [,] 1 ) ) → ( 𝐹 ‘ 0 ) ∈ ( ∪ 𝑅 × ∪ 𝑆 ) )
144 1st2nd2 ⊢ ( ( 𝐹 ‘ 0 ) ∈ ( ∪ 𝑅 × ∪ 𝑆 ) → ( 𝐹 ‘ 0 ) = ⟨ ( 1st ‘ ( 𝐹 ‘ 0 ) ) , ( 2nd ‘ ( 𝐹 ‘ 0 ) ) ⟩ )
145 143 144 syl ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 0 [,] 1 ) ) → ( 𝐹 ‘ 0 ) = ⟨ ( 1st ‘ ( 𝐹 ‘ 0 ) ) , ( 2nd ‘ ( 𝐹 ‘ 0 ) ) ⟩ )
146 142 145 eqtrd ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 0 [,] 1 ) ) → ( ( ( 0 [,] 1 ) × { ( 𝐹 ‘ 0 ) } ) ‘ 𝑠 ) = ⟨ ( 1st ‘ ( 𝐹 ‘ 0 ) ) , ( 2nd ‘ ( 𝐹 ‘ 0 ) ) ⟩ )
147 132 139 146 3eqtr4d ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 0 [,] 1 ) ) → ( 𝑠 ( 𝑥 ∈ ( 0 [,] 1 ) , 𝑦 ∈ ( 0 [,] 1 ) ↦ ⟨ ( 𝑥 𝐺 𝑦 ) , ( 𝑥 𝐻 𝑦 ) ⟩ ) 1 ) = ( ( ( 0 [,] 1 ) × { ( 𝐹 ‘ 0 ) } ) ‘ 𝑠 ) )
148 30 38 6 phtpyi ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 0 [,] 1 ) ) → ( ( 0 𝐺 𝑠 ) = ( 𝐴 ‘ 0 ) ∧ ( 1 𝐺 𝑠 ) = ( 𝐴 ‘ 1 ) ) )
149 148 simpld ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 0 [,] 1 ) ) → ( 0 𝐺 𝑠 ) = ( 𝐴 ‘ 0 ) )
150 149 117 eqtrd ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 0 [,] 1 ) ) → ( 0 𝐺 𝑠 ) = ( 1st ‘ ( 𝐹 ‘ 0 ) ) )
151 53 60 7 phtpyi ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 0 [,] 1 ) ) → ( ( 0 𝐻 𝑠 ) = ( 𝐵 ‘ 0 ) ∧ ( 1 𝐻 𝑠 ) = ( 𝐵 ‘ 1 ) ) )
152 151 simpld ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 0 [,] 1 ) ) → ( 0 𝐻 𝑠 ) = ( 𝐵 ‘ 0 ) )
153 152 130 eqtrd ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 0 [,] 1 ) ) → ( 0 𝐻 𝑠 ) = ( 2nd ‘ ( 𝐹 ‘ 0 ) ) )
154 150 153 opeq12d ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 0 [,] 1 ) ) → ⟨ ( 0 𝐺 𝑠 ) , ( 0 𝐻 𝑠 ) ⟩ = ⟨ ( 1st ‘ ( 𝐹 ‘ 0 ) ) , ( 2nd ‘ ( 𝐹 ‘ 0 ) ) ⟩ )
155 oveq12 ⊢ ( ( 𝑥 = 0 ∧ 𝑦 = 𝑠 ) → ( 𝑥 𝐺 𝑦 ) = ( 0 𝐺 𝑠 ) )
156 oveq12 ⊢ ( ( 𝑥 = 0 ∧ 𝑦 = 𝑠 ) → ( 𝑥 𝐻 𝑦 ) = ( 0 𝐻 𝑠 ) )
157 155 156 opeq12d ⊢ ( ( 𝑥 = 0 ∧ 𝑦 = 𝑠 ) → ⟨ ( 𝑥 𝐺 𝑦 ) , ( 𝑥 𝐻 𝑦 ) ⟩ = ⟨ ( 0 𝐺 𝑠 ) , ( 0 𝐻 𝑠 ) ⟩ )
158 opex ⊢ ⟨ ( 0 𝐺 𝑠 ) , ( 0 𝐻 𝑠 ) ⟩ ∈ V
159 157 99 158 ovmpoa ⊢ ( ( 0 ∈ ( 0 [,] 1 ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) → ( 0 ( 𝑥 ∈ ( 0 [,] 1 ) , 𝑦 ∈ ( 0 [,] 1 ) ↦ ⟨ ( 𝑥 𝐺 𝑦 ) , ( 𝑥 𝐻 𝑦 ) ⟩ ) 𝑠 ) = ⟨ ( 0 𝐺 𝑠 ) , ( 0 𝐻 𝑠 ) ⟩ )
160 21 95 159 sylancr ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 0 [,] 1 ) ) → ( 0 ( 𝑥 ∈ ( 0 [,] 1 ) , 𝑦 ∈ ( 0 [,] 1 ) ↦ ⟨ ( 𝑥 𝐺 𝑦 ) , ( 𝑥 𝐻 𝑦 ) ⟩ ) 𝑠 ) = ⟨ ( 0 𝐺 𝑠 ) , ( 0 𝐻 𝑠 ) ⟩ )
161 154 160 145 3eqtr4d ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 0 [,] 1 ) ) → ( 0 ( 𝑥 ∈ ( 0 [,] 1 ) , 𝑦 ∈ ( 0 [,] 1 ) ↦ ⟨ ( 𝑥 𝐺 𝑦 ) , ( 𝑥 𝐻 𝑦 ) ⟩ ) 𝑠 ) = ( 𝐹 ‘ 0 ) )
162 148 simprd ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 0 [,] 1 ) ) → ( 1 𝐺 𝑠 ) = ( 𝐴 ‘ 1 ) )
163 4 fveq1i ⊢ ( 𝐴 ‘ 1 ) = ( ( ( 1st ↾ ( ∪ 𝑅 × ∪ 𝑆 ) ) ∘ 𝐹 ) ‘ 1 )
164 fvco3 ⊢ ( ( 𝐹 : ( 0 [,] 1 ) ⟶ ( ∪ 𝑅 × ∪ 𝑆 ) ∧ 1 ∈ ( 0 [,] 1 ) ) → ( ( ( 1st ↾ ( ∪ 𝑅 × ∪ 𝑆 ) ) ∘ 𝐹 ) ‘ 1 ) = ( ( 1st ↾ ( ∪ 𝑅 × ∪ 𝑆 ) ) ‘ ( 𝐹 ‘ 1 ) ) )
165 20 133 164 sylancl ⊢ ( 𝜑 → ( ( ( 1st ↾ ( ∪ 𝑅 × ∪ 𝑆 ) ) ∘ 𝐹 ) ‘ 1 ) = ( ( 1st ↾ ( ∪ 𝑅 × ∪ 𝑆 ) ) ‘ ( 𝐹 ‘ 1 ) ) )
166 163 165 syl5eq ⊢ ( 𝜑 → ( 𝐴 ‘ 1 ) = ( ( 1st ↾ ( ∪ 𝑅 × ∪ 𝑆 ) ) ‘ ( 𝐹 ‘ 1 ) ) )
167 ffvelrn ⊢ ( ( 𝐹 : ( 0 [,] 1 ) ⟶ ( ∪ 𝑅 × ∪ 𝑆 ) ∧ 1 ∈ ( 0 [,] 1 ) ) → ( 𝐹 ‘ 1 ) ∈ ( ∪ 𝑅 × ∪ 𝑆 ) )
168 20 133 167 sylancl ⊢ ( 𝜑 → ( 𝐹 ‘ 1 ) ∈ ( ∪ 𝑅 × ∪ 𝑆 ) )
169 fvres ⊢ ( ( 𝐹 ‘ 1 ) ∈ ( ∪ 𝑅 × ∪ 𝑆 ) → ( ( 1st ↾ ( ∪ 𝑅 × ∪ 𝑆 ) ) ‘ ( 𝐹 ‘ 1 ) ) = ( 1st ‘ ( 𝐹 ‘ 1 ) ) )
170 168 169 syl ⊢ ( 𝜑 → ( ( 1st ↾ ( ∪ 𝑅 × ∪ 𝑆 ) ) ‘ ( 𝐹 ‘ 1 ) ) = ( 1st ‘ ( 𝐹 ‘ 1 ) ) )
171 166 170 eqtrd ⊢ ( 𝜑 → ( 𝐴 ‘ 1 ) = ( 1st ‘ ( 𝐹 ‘ 1 ) ) )
172 171 adantr ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 0 [,] 1 ) ) → ( 𝐴 ‘ 1 ) = ( 1st ‘ ( 𝐹 ‘ 1 ) ) )
173 162 172 eqtrd ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 0 [,] 1 ) ) → ( 1 𝐺 𝑠 ) = ( 1st ‘ ( 𝐹 ‘ 1 ) ) )
174 151 simprd ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 0 [,] 1 ) ) → ( 1 𝐻 𝑠 ) = ( 𝐵 ‘ 1 ) )
175 5 fveq1i ⊢ ( 𝐵 ‘ 1 ) = ( ( ( 2nd ↾ ( ∪ 𝑅 × ∪ 𝑆 ) ) ∘ 𝐹 ) ‘ 1 )
176 fvco3 ⊢ ( ( 𝐹 : ( 0 [,] 1 ) ⟶ ( ∪ 𝑅 × ∪ 𝑆 ) ∧ 1 ∈ ( 0 [,] 1 ) ) → ( ( ( 2nd ↾ ( ∪ 𝑅 × ∪ 𝑆 ) ) ∘ 𝐹 ) ‘ 1 ) = ( ( 2nd ↾ ( ∪ 𝑅 × ∪ 𝑆 ) ) ‘ ( 𝐹 ‘ 1 ) ) )
177 20 133 176 sylancl ⊢ ( 𝜑 → ( ( ( 2nd ↾ ( ∪ 𝑅 × ∪ 𝑆 ) ) ∘ 𝐹 ) ‘ 1 ) = ( ( 2nd ↾ ( ∪ 𝑅 × ∪ 𝑆 ) ) ‘ ( 𝐹 ‘ 1 ) ) )
178 175 177 syl5eq ⊢ ( 𝜑 → ( 𝐵 ‘ 1 ) = ( ( 2nd ↾ ( ∪ 𝑅 × ∪ 𝑆 ) ) ‘ ( 𝐹 ‘ 1 ) ) )
179 fvres ⊢ ( ( 𝐹 ‘ 1 ) ∈ ( ∪ 𝑅 × ∪ 𝑆 ) → ( ( 2nd ↾ ( ∪ 𝑅 × ∪ 𝑆 ) ) ‘ ( 𝐹 ‘ 1 ) ) = ( 2nd ‘ ( 𝐹 ‘ 1 ) ) )
180 168 179 syl ⊢ ( 𝜑 → ( ( 2nd ↾ ( ∪ 𝑅 × ∪ 𝑆 ) ) ‘ ( 𝐹 ‘ 1 ) ) = ( 2nd ‘ ( 𝐹 ‘ 1 ) ) )
181 178 180 eqtrd ⊢ ( 𝜑 → ( 𝐵 ‘ 1 ) = ( 2nd ‘ ( 𝐹 ‘ 1 ) ) )
182 181 adantr ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 0 [,] 1 ) ) → ( 𝐵 ‘ 1 ) = ( 2nd ‘ ( 𝐹 ‘ 1 ) ) )
183 174 182 eqtrd ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 0 [,] 1 ) ) → ( 1 𝐻 𝑠 ) = ( 2nd ‘ ( 𝐹 ‘ 1 ) ) )
184 173 183 opeq12d ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 0 [,] 1 ) ) → ⟨ ( 1 𝐺 𝑠 ) , ( 1 𝐻 𝑠 ) ⟩ = ⟨ ( 1st ‘ ( 𝐹 ‘ 1 ) ) , ( 2nd ‘ ( 𝐹 ‘ 1 ) ) ⟩ )
185 oveq12 ⊢ ( ( 𝑥 = 1 ∧ 𝑦 = 𝑠 ) → ( 𝑥 𝐺 𝑦 ) = ( 1 𝐺 𝑠 ) )
186 oveq12 ⊢ ( ( 𝑥 = 1 ∧ 𝑦 = 𝑠 ) → ( 𝑥 𝐻 𝑦 ) = ( 1 𝐻 𝑠 ) )
187 185 186 opeq12d ⊢ ( ( 𝑥 = 1 ∧ 𝑦 = 𝑠 ) → ⟨ ( 𝑥 𝐺 𝑦 ) , ( 𝑥 𝐻 𝑦 ) ⟩ = ⟨ ( 1 𝐺 𝑠 ) , ( 1 𝐻 𝑠 ) ⟩ )
188 opex ⊢ ⟨ ( 1 𝐺 𝑠 ) , ( 1 𝐻 𝑠 ) ⟩ ∈ V
189 187 99 188 ovmpoa ⊢ ( ( 1 ∈ ( 0 [,] 1 ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) → ( 1 ( 𝑥 ∈ ( 0 [,] 1 ) , 𝑦 ∈ ( 0 [,] 1 ) ↦ ⟨ ( 𝑥 𝐺 𝑦 ) , ( 𝑥 𝐻 𝑦 ) ⟩ ) 𝑠 ) = ⟨ ( 1 𝐺 𝑠 ) , ( 1 𝐻 𝑠 ) ⟩ )
190 133 95 189 sylancr ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 0 [,] 1 ) ) → ( 1 ( 𝑥 ∈ ( 0 [,] 1 ) , 𝑦 ∈ ( 0 [,] 1 ) ↦ ⟨ ( 𝑥 𝐺 𝑦 ) , ( 𝑥 𝐻 𝑦 ) ⟩ ) 𝑠 ) = ⟨ ( 1 𝐺 𝑠 ) , ( 1 𝐻 𝑠 ) ⟩ )
191 168 adantr ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 0 [,] 1 ) ) → ( 𝐹 ‘ 1 ) ∈ ( ∪ 𝑅 × ∪ 𝑆 ) )
192 1st2nd2 ⊢ ( ( 𝐹 ‘ 1 ) ∈ ( ∪ 𝑅 × ∪ 𝑆 ) → ( 𝐹 ‘ 1 ) = ⟨ ( 1st ‘ ( 𝐹 ‘ 1 ) ) , ( 2nd ‘ ( 𝐹 ‘ 1 ) ) ⟩ )
193 191 192 syl ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 0 [,] 1 ) ) → ( 𝐹 ‘ 1 ) = ⟨ ( 1st ‘ ( 𝐹 ‘ 1 ) ) , ( 2nd ‘ ( 𝐹 ‘ 1 ) ) ⟩ )
194 184 190 193 3eqtr4d ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 0 [,] 1 ) ) → ( 1 ( 𝑥 ∈ ( 0 [,] 1 ) , 𝑦 ∈ ( 0 [,] 1 ) ↦ ⟨ ( 𝑥 𝐺 𝑦 ) , ( 𝑥 𝐻 𝑦 ) ⟩ ) 𝑠 ) = ( 𝐹 ‘ 1 ) )
195 3 25 69 105 147 161 194 isphtpy2d ⊢ ( 𝜑 → ( 𝑥 ∈ ( 0 [,] 1 ) , 𝑦 ∈ ( 0 [,] 1 ) ↦ ⟨ ( 𝑥 𝐺 𝑦 ) , ( 𝑥 𝐻 𝑦 ) ⟩ ) ∈ ( 𝐹 ( PHtpy ‘ ( 𝑅 ×t 𝑆 ) ) ( ( 0 [,] 1 ) × { ( 𝐹 ‘ 0 ) } ) ) )
196 195 ne0d ⊢ ( 𝜑 → ( 𝐹 ( PHtpy ‘ ( 𝑅 ×t 𝑆 ) ) ( ( 0 [,] 1 ) × { ( 𝐹 ‘ 0 ) } ) ) ≠ ∅ )
197 isphtpc ⊢ ( 𝐹 ( ≃ph ‘ ( 𝑅 ×t 𝑆 ) ) ( ( 0 [,] 1 ) × { ( 𝐹 ‘ 0 ) } ) ↔ ( 𝐹 ∈ ( II Cn ( 𝑅 ×t 𝑆 ) ) ∧ ( ( 0 [,] 1 ) × { ( 𝐹 ‘ 0 ) } ) ∈ ( II Cn ( 𝑅 ×t 𝑆 ) ) ∧ ( 𝐹 ( PHtpy ‘ ( 𝑅 ×t 𝑆 ) ) ( ( 0 [,] 1 ) × { ( 𝐹 ‘ 0 ) } ) ) ≠ ∅ ) )
198 3 25 196 197 syl3anbrc ⊢ ( 𝜑 → 𝐹 ( ≃ph ‘ ( 𝑅 ×t 𝑆 ) ) ( ( 0 [,] 1 ) × { ( 𝐹 ‘ 0 ) } ) )