Metamath Proof Explorer

Theorem rntpos

Description: The range of tpos F when dom F is a relation. (Contributed by Mario Carneiro, 10-Sep-2015)

Ref Expression
Assertion rntpos ( Rel dom 𝐹 → ran tpos 𝐹 = ran 𝐹 )

Proof

Step Hyp Ref Expression
1 vex ⊢ 𝑧 ∈ V
2 1 elrn ⊢ ( 𝑧 ∈ ran tpos 𝐹 ↔ ∃ 𝑤 𝑤 tpos 𝐹 𝑧 )
3 vex ⊢ 𝑤 ∈ V
4 3 1 breldm ⊢ ( 𝑤 tpos 𝐹 𝑧 → 𝑤 ∈ dom tpos 𝐹 )
5 dmtpos ⊢ ( Rel dom 𝐹 → dom tpos 𝐹 = ◡ dom 𝐹 )
6 5 eleq2d ⊢ ( Rel dom 𝐹 → ( 𝑤 ∈ dom tpos 𝐹 ↔ 𝑤 ∈ ◡ dom 𝐹 ) )
7 4 6 syl5ib ⊢ ( Rel dom 𝐹 → ( 𝑤 tpos 𝐹 𝑧 → 𝑤 ∈ ◡ dom 𝐹 ) )
8 relcnv ⊢ Rel ◡ dom 𝐹
9 elrel ⊢ ( ( Rel ◡ dom 𝐹 ∧ 𝑤 ∈ ◡ dom 𝐹 ) → ∃ 𝑥 ∃ 𝑦 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ )
10 8 9 mpan ⊢ ( 𝑤 ∈ ◡ dom 𝐹 → ∃ 𝑥 ∃ 𝑦 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ )
11 7 10 syl6 ⊢ ( Rel dom 𝐹 → ( 𝑤 tpos 𝐹 𝑧 → ∃ 𝑥 ∃ 𝑦 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ ) )
12 breq1 ⊢ ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝑤 tpos 𝐹 𝑧 ↔ ⟨ 𝑥 , 𝑦 ⟩ tpos 𝐹 𝑧 ) )
13 brtpos ⊢ ( 𝑧 ∈ V → ( ⟨ 𝑥 , 𝑦 ⟩ tpos 𝐹 𝑧 ↔ ⟨ 𝑦 , 𝑥 ⟩ 𝐹 𝑧 ) )
14 13 elv ⊢ ( ⟨ 𝑥 , 𝑦 ⟩ tpos 𝐹 𝑧 ↔ ⟨ 𝑦 , 𝑥 ⟩ 𝐹 𝑧 )
15 12 14 bitrdi ⊢ ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝑤 tpos 𝐹 𝑧 ↔ ⟨ 𝑦 , 𝑥 ⟩ 𝐹 𝑧 ) )
16 opex ⊢ ⟨ 𝑦 , 𝑥 ⟩ ∈ V
17 16 1 brelrn ⊢ ( ⟨ 𝑦 , 𝑥 ⟩ 𝐹 𝑧 → 𝑧 ∈ ran 𝐹 )
18 15 17 syl6bi ⊢ ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝑤 tpos 𝐹 𝑧 → 𝑧 ∈ ran 𝐹 ) )
19 18 exlimivv ⊢ ( ∃ 𝑥 ∃ 𝑦 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝑤 tpos 𝐹 𝑧 → 𝑧 ∈ ran 𝐹 ) )
20 11 19 syli ⊢ ( Rel dom 𝐹 → ( 𝑤 tpos 𝐹 𝑧 → 𝑧 ∈ ran 𝐹 ) )
21 20 exlimdv ⊢ ( Rel dom 𝐹 → ( ∃ 𝑤 𝑤 tpos 𝐹 𝑧 → 𝑧 ∈ ran 𝐹 ) )
22 2 21 syl5bi ⊢ ( Rel dom 𝐹 → ( 𝑧 ∈ ran tpos 𝐹 → 𝑧 ∈ ran 𝐹 ) )
23 1 elrn ⊢ ( 𝑧 ∈ ran 𝐹 ↔ ∃ 𝑤 𝑤 𝐹 𝑧 )
24 3 1 breldm ⊢ ( 𝑤 𝐹 𝑧 → 𝑤 ∈ dom 𝐹 )
25 elrel ⊢ ( ( Rel dom 𝐹 ∧ 𝑤 ∈ dom 𝐹 ) → ∃ 𝑦 ∃ 𝑥 𝑤 = ⟨ 𝑦 , 𝑥 ⟩ )
26 25 ex ⊢ ( Rel dom 𝐹 → ( 𝑤 ∈ dom 𝐹 → ∃ 𝑦 ∃ 𝑥 𝑤 = ⟨ 𝑦 , 𝑥 ⟩ ) )
27 24 26 syl5 ⊢ ( Rel dom 𝐹 → ( 𝑤 𝐹 𝑧 → ∃ 𝑦 ∃ 𝑥 𝑤 = ⟨ 𝑦 , 𝑥 ⟩ ) )
28 breq1 ⊢ ( 𝑤 = ⟨ 𝑦 , 𝑥 ⟩ → ( 𝑤 𝐹 𝑧 ↔ ⟨ 𝑦 , 𝑥 ⟩ 𝐹 𝑧 ) )
29 28 14 bitr4di ⊢ ( 𝑤 = ⟨ 𝑦 , 𝑥 ⟩ → ( 𝑤 𝐹 𝑧 ↔ ⟨ 𝑥 , 𝑦 ⟩ tpos 𝐹 𝑧 ) )
30 opex ⊢ ⟨ 𝑥 , 𝑦 ⟩ ∈ V
31 30 1 brelrn ⊢ ( ⟨ 𝑥 , 𝑦 ⟩ tpos 𝐹 𝑧 → 𝑧 ∈ ran tpos 𝐹 )
32 29 31 syl6bi ⊢ ( 𝑤 = ⟨ 𝑦 , 𝑥 ⟩ → ( 𝑤 𝐹 𝑧 → 𝑧 ∈ ran tpos 𝐹 ) )
33 32 exlimivv ⊢ ( ∃ 𝑦 ∃ 𝑥 𝑤 = ⟨ 𝑦 , 𝑥 ⟩ → ( 𝑤 𝐹 𝑧 → 𝑧 ∈ ran tpos 𝐹 ) )
34 27 33 syli ⊢ ( Rel dom 𝐹 → ( 𝑤 𝐹 𝑧 → 𝑧 ∈ ran tpos 𝐹 ) )
35 34 exlimdv ⊢ ( Rel dom 𝐹 → ( ∃ 𝑤 𝑤 𝐹 𝑧 → 𝑧 ∈ ran tpos 𝐹 ) )
36 23 35 syl5bi ⊢ ( Rel dom 𝐹 → ( 𝑧 ∈ ran 𝐹 → 𝑧 ∈ ran tpos 𝐹 ) )
37 22 36 impbid ⊢ ( Rel dom 𝐹 → ( 𝑧 ∈ ran tpos 𝐹 ↔ 𝑧 ∈ ran 𝐹 ) )
38 37 eqrdv ⊢ ( Rel dom 𝐹 → ran tpos 𝐹 = ran 𝐹 )