Metamath Proof Explorer

Theorem grtrimap

Description: Conditions for mapping triangles onto triangles. Lemma for grimgrtri and grlimgrtri . (Contributed by AV, 23-Aug-2025)

Ref Expression
Assertion grtrimap ( 𝐹 : 𝑉 –1-1→ 𝑊 → ( ( ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) ∧ ( 𝑇 = { 𝑎 , 𝑏 , 𝑐 } ∧ ( ♯ ‘ 𝑇 ) = 3 ) ) → ( ( ( 𝐹 ‘ 𝑎 ) ∈ 𝑊 ∧ ( 𝐹 ‘ 𝑏 ) ∈ 𝑊 ∧ ( 𝐹 ‘ 𝑐 ) ∈ 𝑊 ) ∧ ( 𝐹 “ 𝑇 ) = { ( 𝐹 ‘ 𝑎 ) , ( 𝐹 ‘ 𝑏 ) , ( 𝐹 ‘ 𝑐 ) } ∧ ( ♯ ‘ ( 𝐹 “ 𝑇 ) ) = 3 ) ) )

Proof

Step Hyp Ref Expression
1 f1f ⊢ ( 𝐹 : 𝑉 –1-1→ 𝑊 → 𝐹 : 𝑉 ⟶ 𝑊 )
2 1 ffvelcdmda ⊢ ( ( 𝐹 : 𝑉 –1-1→ 𝑊 ∧ 𝑎 ∈ 𝑉 ) → ( 𝐹 ‘ 𝑎 ) ∈ 𝑊 )
3 2 ex ⊢ ( 𝐹 : 𝑉 –1-1→ 𝑊 → ( 𝑎 ∈ 𝑉 → ( 𝐹 ‘ 𝑎 ) ∈ 𝑊 ) )
4 1 ffvelcdmda ⊢ ( ( 𝐹 : 𝑉 –1-1→ 𝑊 ∧ 𝑏 ∈ 𝑉 ) → ( 𝐹 ‘ 𝑏 ) ∈ 𝑊 )
5 4 ex ⊢ ( 𝐹 : 𝑉 –1-1→ 𝑊 → ( 𝑏 ∈ 𝑉 → ( 𝐹 ‘ 𝑏 ) ∈ 𝑊 ) )
6 1 ffvelcdmda ⊢ ( ( 𝐹 : 𝑉 –1-1→ 𝑊 ∧ 𝑐 ∈ 𝑉 ) → ( 𝐹 ‘ 𝑐 ) ∈ 𝑊 )
7 6 ex ⊢ ( 𝐹 : 𝑉 –1-1→ 𝑊 → ( 𝑐 ∈ 𝑉 → ( 𝐹 ‘ 𝑐 ) ∈ 𝑊 ) )
8 3 5 7 3anim123d ⊢ ( 𝐹 : 𝑉 –1-1→ 𝑊 → ( ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) → ( ( 𝐹 ‘ 𝑎 ) ∈ 𝑊 ∧ ( 𝐹 ‘ 𝑏 ) ∈ 𝑊 ∧ ( 𝐹 ‘ 𝑐 ) ∈ 𝑊 ) ) )
9 8 adantrd ⊢ ( 𝐹 : 𝑉 –1-1→ 𝑊 → ( ( ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) ∧ ( 𝑇 = { 𝑎 , 𝑏 , 𝑐 } ∧ ( ♯ ‘ 𝑇 ) = 3 ) ) → ( ( 𝐹 ‘ 𝑎 ) ∈ 𝑊 ∧ ( 𝐹 ‘ 𝑏 ) ∈ 𝑊 ∧ ( 𝐹 ‘ 𝑐 ) ∈ 𝑊 ) ) )
10 9 imp ⊢ ( ( 𝐹 : 𝑉 –1-1→ 𝑊 ∧ ( ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) ∧ ( 𝑇 = { 𝑎 , 𝑏 , 𝑐 } ∧ ( ♯ ‘ 𝑇 ) = 3 ) ) ) → ( ( 𝐹 ‘ 𝑎 ) ∈ 𝑊 ∧ ( 𝐹 ‘ 𝑏 ) ∈ 𝑊 ∧ ( 𝐹 ‘ 𝑐 ) ∈ 𝑊 ) )
11 imaeq2 ⊢ ( 𝑇 = { 𝑎 , 𝑏 , 𝑐 } → ( 𝐹 “ 𝑇 ) = ( 𝐹 “ { 𝑎 , 𝑏 , 𝑐 } ) )
12 11 ad2antrl ⊢ ( ( ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) ∧ ( 𝑇 = { 𝑎 , 𝑏 , 𝑐 } ∧ ( ♯ ‘ 𝑇 ) = 3 ) ) → ( 𝐹 “ 𝑇 ) = ( 𝐹 “ { 𝑎 , 𝑏 , 𝑐 } ) )
13 12 adantl ⊢ ( ( 𝐹 : 𝑉 –1-1→ 𝑊 ∧ ( ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) ∧ ( 𝑇 = { 𝑎 , 𝑏 , 𝑐 } ∧ ( ♯ ‘ 𝑇 ) = 3 ) ) ) → ( 𝐹 “ 𝑇 ) = ( 𝐹 “ { 𝑎 , 𝑏 , 𝑐 } ) )
14 f1fn ⊢ ( 𝐹 : 𝑉 –1-1→ 𝑊 → 𝐹 Fn 𝑉 )
15 14 adantr ⊢ ( ( 𝐹 : 𝑉 –1-1→ 𝑊 ∧ ( ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) ∧ ( 𝑇 = { 𝑎 , 𝑏 , 𝑐 } ∧ ( ♯ ‘ 𝑇 ) = 3 ) ) ) → 𝐹 Fn 𝑉 )
16 simprl1 ⊢ ( ( 𝐹 : 𝑉 –1-1→ 𝑊 ∧ ( ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) ∧ ( 𝑇 = { 𝑎 , 𝑏 , 𝑐 } ∧ ( ♯ ‘ 𝑇 ) = 3 ) ) ) → 𝑎 ∈ 𝑉 )
17 simprl2 ⊢ ( ( 𝐹 : 𝑉 –1-1→ 𝑊 ∧ ( ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) ∧ ( 𝑇 = { 𝑎 , 𝑏 , 𝑐 } ∧ ( ♯ ‘ 𝑇 ) = 3 ) ) ) → 𝑏 ∈ 𝑉 )
18 simprl3 ⊢ ( ( 𝐹 : 𝑉 –1-1→ 𝑊 ∧ ( ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) ∧ ( 𝑇 = { 𝑎 , 𝑏 , 𝑐 } ∧ ( ♯ ‘ 𝑇 ) = 3 ) ) ) → 𝑐 ∈ 𝑉 )
19 15 16 17 18 fnimatpd ⊢ ( ( 𝐹 : 𝑉 –1-1→ 𝑊 ∧ ( ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) ∧ ( 𝑇 = { 𝑎 , 𝑏 , 𝑐 } ∧ ( ♯ ‘ 𝑇 ) = 3 ) ) ) → ( 𝐹 “ { 𝑎 , 𝑏 , 𝑐 } ) = { ( 𝐹 ‘ 𝑎 ) , ( 𝐹 ‘ 𝑏 ) , ( 𝐹 ‘ 𝑐 ) } )
20 13 19 eqtrd ⊢ ( ( 𝐹 : 𝑉 –1-1→ 𝑊 ∧ ( ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) ∧ ( 𝑇 = { 𝑎 , 𝑏 , 𝑐 } ∧ ( ♯ ‘ 𝑇 ) = 3 ) ) ) → ( 𝐹 “ 𝑇 ) = { ( 𝐹 ‘ 𝑎 ) , ( 𝐹 ‘ 𝑏 ) , ( 𝐹 ‘ 𝑐 ) } )
21 simpl ⊢ ( ( 𝐹 : 𝑉 –1-1→ 𝑊 ∧ ( ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) ∧ ( 𝑇 = { 𝑎 , 𝑏 , 𝑐 } ∧ ( ♯ ‘ 𝑇 ) = 3 ) ) ) → 𝐹 : 𝑉 –1-1→ 𝑊 )
22 tpssi ⊢ ( ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) → { 𝑎 , 𝑏 , 𝑐 } ⊆ 𝑉 )
23 22 adantr ⊢ ( ( ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) ∧ ( 𝑇 = { 𝑎 , 𝑏 , 𝑐 } ∧ ( ♯ ‘ 𝑇 ) = 3 ) ) → { 𝑎 , 𝑏 , 𝑐 } ⊆ 𝑉 )
24 sseq1 ⊢ ( 𝑇 = { 𝑎 , 𝑏 , 𝑐 } → ( 𝑇 ⊆ 𝑉 ↔ { 𝑎 , 𝑏 , 𝑐 } ⊆ 𝑉 ) )
25 24 ad2antrl ⊢ ( ( ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) ∧ ( 𝑇 = { 𝑎 , 𝑏 , 𝑐 } ∧ ( ♯ ‘ 𝑇 ) = 3 ) ) → ( 𝑇 ⊆ 𝑉 ↔ { 𝑎 , 𝑏 , 𝑐 } ⊆ 𝑉 ) )
26 23 25 mpbird ⊢ ( ( ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) ∧ ( 𝑇 = { 𝑎 , 𝑏 , 𝑐 } ∧ ( ♯ ‘ 𝑇 ) = 3 ) ) → 𝑇 ⊆ 𝑉 )
27 26 adantl ⊢ ( ( 𝐹 : 𝑉 –1-1→ 𝑊 ∧ ( ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) ∧ ( 𝑇 = { 𝑎 , 𝑏 , 𝑐 } ∧ ( ♯ ‘ 𝑇 ) = 3 ) ) ) → 𝑇 ⊆ 𝑉 )
28 tpex ⊢ { 𝑎 , 𝑏 , 𝑐 } ∈ V
29 eleq1 ⊢ ( 𝑇 = { 𝑎 , 𝑏 , 𝑐 } → ( 𝑇 ∈ V ↔ { 𝑎 , 𝑏 , 𝑐 } ∈ V ) )
30 28 29 mpbiri ⊢ ( 𝑇 = { 𝑎 , 𝑏 , 𝑐 } → 𝑇 ∈ V )
31 30 ad2antrl ⊢ ( ( ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) ∧ ( 𝑇 = { 𝑎 , 𝑏 , 𝑐 } ∧ ( ♯ ‘ 𝑇 ) = 3 ) ) → 𝑇 ∈ V )
32 31 adantl ⊢ ( ( 𝐹 : 𝑉 –1-1→ 𝑊 ∧ ( ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) ∧ ( 𝑇 = { 𝑎 , 𝑏 , 𝑐 } ∧ ( ♯ ‘ 𝑇 ) = 3 ) ) ) → 𝑇 ∈ V )
33 f1imaeng ⊢ ( ( 𝐹 : 𝑉 –1-1→ 𝑊 ∧ 𝑇 ⊆ 𝑉 ∧ 𝑇 ∈ V ) → ( 𝐹 “ 𝑇 ) ≈ 𝑇 )
34 hasheni ⊢ ( ( 𝐹 “ 𝑇 ) ≈ 𝑇 → ( ♯ ‘ ( 𝐹 “ 𝑇 ) ) = ( ♯ ‘ 𝑇 ) )
35 33 34 syl ⊢ ( ( 𝐹 : 𝑉 –1-1→ 𝑊 ∧ 𝑇 ⊆ 𝑉 ∧ 𝑇 ∈ V ) → ( ♯ ‘ ( 𝐹 “ 𝑇 ) ) = ( ♯ ‘ 𝑇 ) )
36 35 eqcomd ⊢ ( ( 𝐹 : 𝑉 –1-1→ 𝑊 ∧ 𝑇 ⊆ 𝑉 ∧ 𝑇 ∈ V ) → ( ♯ ‘ 𝑇 ) = ( ♯ ‘ ( 𝐹 “ 𝑇 ) ) )
37 21 27 32 36 syl3anc ⊢ ( ( 𝐹 : 𝑉 –1-1→ 𝑊 ∧ ( ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) ∧ ( 𝑇 = { 𝑎 , 𝑏 , 𝑐 } ∧ ( ♯ ‘ 𝑇 ) = 3 ) ) ) → ( ♯ ‘ 𝑇 ) = ( ♯ ‘ ( 𝐹 “ 𝑇 ) ) )
38 simprrr ⊢ ( ( 𝐹 : 𝑉 –1-1→ 𝑊 ∧ ( ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) ∧ ( 𝑇 = { 𝑎 , 𝑏 , 𝑐 } ∧ ( ♯ ‘ 𝑇 ) = 3 ) ) ) → ( ♯ ‘ 𝑇 ) = 3 )
39 37 38 eqtr3d ⊢ ( ( 𝐹 : 𝑉 –1-1→ 𝑊 ∧ ( ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) ∧ ( 𝑇 = { 𝑎 , 𝑏 , 𝑐 } ∧ ( ♯ ‘ 𝑇 ) = 3 ) ) ) → ( ♯ ‘ ( 𝐹 “ 𝑇 ) ) = 3 )
40 10 20 39 3jca ⊢ ( ( 𝐹 : 𝑉 –1-1→ 𝑊 ∧ ( ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) ∧ ( 𝑇 = { 𝑎 , 𝑏 , 𝑐 } ∧ ( ♯ ‘ 𝑇 ) = 3 ) ) ) → ( ( ( 𝐹 ‘ 𝑎 ) ∈ 𝑊 ∧ ( 𝐹 ‘ 𝑏 ) ∈ 𝑊 ∧ ( 𝐹 ‘ 𝑐 ) ∈ 𝑊 ) ∧ ( 𝐹 “ 𝑇 ) = { ( 𝐹 ‘ 𝑎 ) , ( 𝐹 ‘ 𝑏 ) , ( 𝐹 ‘ 𝑐 ) } ∧ ( ♯ ‘ ( 𝐹 “ 𝑇 ) ) = 3 ) )
41 40 ex ⊢ ( 𝐹 : 𝑉 –1-1→ 𝑊 → ( ( ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) ∧ ( 𝑇 = { 𝑎 , 𝑏 , 𝑐 } ∧ ( ♯ ‘ 𝑇 ) = 3 ) ) → ( ( ( 𝐹 ‘ 𝑎 ) ∈ 𝑊 ∧ ( 𝐹 ‘ 𝑏 ) ∈ 𝑊 ∧ ( 𝐹 ‘ 𝑐 ) ∈ 𝑊 ) ∧ ( 𝐹 “ 𝑇 ) = { ( 𝐹 ‘ 𝑎 ) , ( 𝐹 ‘ 𝑏 ) , ( 𝐹 ‘ 𝑐 ) } ∧ ( ♯ ‘ ( 𝐹 “ 𝑇 ) ) = 3 ) ) )