ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  upxp GIF version

Theorem upxp 13933
Description: Universal property of the Cartesian product considered as a categorical product in the category of sets. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 27-Dec-2014.)
Hypotheses
Ref Expression
upxp.1 š‘ƒ = (1st ↾ (šµ Ɨ š¶))
upxp.2 š‘„ = (2nd ↾ (šµ Ɨ š¶))
Assertion
Ref Expression
upxp ((š“ ∈ š· ∧ š¹:š“āŸ¶šµ ∧ šŗ:š“āŸ¶š¶) → ∃!ā„Ž(ā„Ž:š“āŸ¶(šµ Ɨ š¶) ∧ š¹ = (š‘ƒ ∘ ā„Ž) ∧ šŗ = (š‘„ ∘ ā„Ž)))
Distinct variable groups:   š“,ā„Ž   šµ,ā„Ž   š¶,ā„Ž   ā„Ž,š¹   ā„Ž,šŗ   š·,ā„Ž
Allowed substitution hints:   š‘ƒ(ā„Ž)   š‘„(ā„Ž)

Proof of Theorem upxp
Dummy variables š‘„ š‘§ are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 mptexg 5744 . . . 4 (š“ ∈ š· → (š‘„ ∈ š“ ↦ ⟨(š¹ā€˜š‘„), (šŗā€˜š‘„)⟩) ∈ V)
2 eueq 2910 . . . 4 ((š‘„ ∈ š“ ↦ ⟨(š¹ā€˜š‘„), (šŗā€˜š‘„)⟩) ∈ V ↔ ∃!ā„Ž ā„Ž = (š‘„ ∈ š“ ↦ ⟨(š¹ā€˜š‘„), (šŗā€˜š‘„)⟩))
31, 2sylib 122 . . 3 (š“ ∈ š· → ∃!ā„Ž ā„Ž = (š‘„ ∈ š“ ↦ ⟨(š¹ā€˜š‘„), (šŗā€˜š‘„)⟩))
433ad2ant1 1018 . 2 ((š“ ∈ š· ∧ š¹:š“āŸ¶šµ ∧ šŗ:š“āŸ¶š¶) → ∃!ā„Ž ā„Ž = (š‘„ ∈ š“ ↦ ⟨(š¹ā€˜š‘„), (šŗā€˜š‘„)⟩))
5 ffn 5367 . . . . . . . 8 (ā„Ž:š“āŸ¶(šµ Ɨ š¶) → ā„Ž Fn š“)
653ad2ant1 1018 . . . . . . 7 ((ā„Ž:š“āŸ¶(šµ Ɨ š¶) ∧ š¹ = (š‘ƒ ∘ ā„Ž) ∧ šŗ = (š‘„ ∘ ā„Ž)) → ā„Ž Fn š“)
76adantl 277 . . . . . 6 (((š“ ∈ š· ∧ š¹:š“āŸ¶šµ ∧ šŗ:š“āŸ¶š¶) ∧ (ā„Ž:š“āŸ¶(šµ Ɨ š¶) ∧ š¹ = (š‘ƒ ∘ ā„Ž) ∧ šŗ = (š‘„ ∘ ā„Ž))) → ā„Ž Fn š“)
8 ffvelcdm 5652 . . . . . . . . . . . . 13 ((š¹:š“āŸ¶šµ ∧ š‘„ ∈ š“) → (š¹ā€˜š‘„) ∈ šµ)
9 ffvelcdm 5652 . . . . . . . . . . . . 13 ((šŗ:š“āŸ¶š¶ ∧ š‘„ ∈ š“) → (šŗā€˜š‘„) ∈ š¶)
10 opelxpi 4660 . . . . . . . . . . . . 13 (((š¹ā€˜š‘„) ∈ šµ ∧ (šŗā€˜š‘„) ∈ š¶) → ⟨(š¹ā€˜š‘„), (šŗā€˜š‘„)⟩ ∈ (šµ Ɨ š¶))
118, 9, 10syl2an 289 . . . . . . . . . . . 12 (((š¹:š“āŸ¶šµ ∧ š‘„ ∈ š“) ∧ (šŗ:š“āŸ¶š¶ ∧ š‘„ ∈ š“)) → ⟨(š¹ā€˜š‘„), (šŗā€˜š‘„)⟩ ∈ (šµ Ɨ š¶))
1211anandirs 593 . . . . . . . . . . 11 (((š¹:š“āŸ¶šµ ∧ šŗ:š“āŸ¶š¶) ∧ š‘„ ∈ š“) → ⟨(š¹ā€˜š‘„), (šŗā€˜š‘„)⟩ ∈ (šµ Ɨ š¶))
1312ralrimiva 2550 . . . . . . . . . 10 ((š¹:š“āŸ¶šµ ∧ šŗ:š“āŸ¶š¶) → āˆ€š‘„ ∈ š“ ⟨(š¹ā€˜š‘„), (šŗā€˜š‘„)⟩ ∈ (šµ Ɨ š¶))
14133adant1 1015 . . . . . . . . 9 ((š“ ∈ š· ∧ š¹:š“āŸ¶šµ ∧ šŗ:š“āŸ¶š¶) → āˆ€š‘„ ∈ š“ ⟨(š¹ā€˜š‘„), (šŗā€˜š‘„)⟩ ∈ (šµ Ɨ š¶))
15 eqid 2177 . . . . . . . . . 10 (š‘„ ∈ š“ ↦ ⟨(š¹ā€˜š‘„), (šŗā€˜š‘„)⟩) = (š‘„ ∈ š“ ↦ ⟨(š¹ā€˜š‘„), (šŗā€˜š‘„)⟩)
1615fmpt 5669 . . . . . . . . 9 (āˆ€š‘„ ∈ š“ ⟨(š¹ā€˜š‘„), (šŗā€˜š‘„)⟩ ∈ (šµ Ɨ š¶) ↔ (š‘„ ∈ š“ ↦ ⟨(š¹ā€˜š‘„), (šŗā€˜š‘„)⟩):š“āŸ¶(šµ Ɨ š¶))
1714, 16sylib 122 . . . . . . . 8 ((š“ ∈ š· ∧ š¹:š“āŸ¶šµ ∧ šŗ:š“āŸ¶š¶) → (š‘„ ∈ š“ ↦ ⟨(š¹ā€˜š‘„), (šŗā€˜š‘„)⟩):š“āŸ¶(šµ Ɨ š¶))
1817ffnd 5368 . . . . . . 7 ((š“ ∈ š· ∧ š¹:š“āŸ¶šµ ∧ šŗ:š“āŸ¶š¶) → (š‘„ ∈ š“ ↦ ⟨(š¹ā€˜š‘„), (šŗā€˜š‘„)⟩) Fn š“)
1918adantr 276 . . . . . 6 (((š“ ∈ š· ∧ š¹:š“āŸ¶šµ ∧ šŗ:š“āŸ¶š¶) ∧ (ā„Ž:š“āŸ¶(šµ Ɨ š¶) ∧ š¹ = (š‘ƒ ∘ ā„Ž) ∧ šŗ = (š‘„ ∘ ā„Ž))) → (š‘„ ∈ š“ ↦ ⟨(š¹ā€˜š‘„), (šŗā€˜š‘„)⟩) Fn š“)
20 xpss 4736 . . . . . . . . . . 11 (šµ Ɨ š¶) āŠ† (V Ɨ V)
21 ffvelcdm 5652 . . . . . . . . . . 11 ((ā„Ž:š“āŸ¶(šµ Ɨ š¶) ∧ š‘§ ∈ š“) → (ā„Žā€˜š‘§) ∈ (šµ Ɨ š¶))
2220, 21sselid 3155 . . . . . . . . . 10 ((ā„Ž:š“āŸ¶(šµ Ɨ š¶) ∧ š‘§ ∈ š“) → (ā„Žā€˜š‘§) ∈ (V Ɨ V))
23223ad2antl1 1159 . . . . . . . . 9 (((ā„Ž:š“āŸ¶(šµ Ɨ š¶) ∧ š¹ = (š‘ƒ ∘ ā„Ž) ∧ šŗ = (š‘„ ∘ ā„Ž)) ∧ š‘§ ∈ š“) → (ā„Žā€˜š‘§) ∈ (V Ɨ V))
2423adantll 476 . . . . . . . 8 ((((š“ ∈ š· ∧ š¹:š“āŸ¶šµ ∧ šŗ:š“āŸ¶š¶) ∧ (ā„Ž:š“āŸ¶(šµ Ɨ š¶) ∧ š¹ = (š‘ƒ ∘ ā„Ž) ∧ šŗ = (š‘„ ∘ ā„Ž))) ∧ š‘§ ∈ š“) → (ā„Žā€˜š‘§) ∈ (V Ɨ V))
25 fveq1 5516 . . . . . . . . . . . 12 (š¹ = (š‘ƒ ∘ ā„Ž) → (š¹ā€˜š‘§) = ((š‘ƒ ∘ ā„Ž)ā€˜š‘§))
26 upxp.1 . . . . . . . . . . . . . 14 š‘ƒ = (1st ↾ (šµ Ɨ š¶))
2726coeq1i 4788 . . . . . . . . . . . . 13 (š‘ƒ ∘ ā„Ž) = ((1st ↾ (šµ Ɨ š¶)) ∘ ā„Ž)
2827fveq1i 5518 . . . . . . . . . . . 12 ((š‘ƒ ∘ ā„Ž)ā€˜š‘§) = (((1st ↾ (šµ Ɨ š¶)) ∘ ā„Ž)ā€˜š‘§)
2925, 28eqtrdi 2226 . . . . . . . . . . 11 (š¹ = (š‘ƒ ∘ ā„Ž) → (š¹ā€˜š‘§) = (((1st ↾ (šµ Ɨ š¶)) ∘ ā„Ž)ā€˜š‘§))
30293ad2ant2 1019 . . . . . . . . . 10 ((ā„Ž:š“āŸ¶(šµ Ɨ š¶) ∧ š¹ = (š‘ƒ ∘ ā„Ž) ∧ šŗ = (š‘„ ∘ ā„Ž)) → (š¹ā€˜š‘§) = (((1st ↾ (šµ Ɨ š¶)) ∘ ā„Ž)ā€˜š‘§))
3130ad2antlr 489 . . . . . . . . 9 ((((š“ ∈ š· ∧ š¹:š“āŸ¶šµ ∧ šŗ:š“āŸ¶š¶) ∧ (ā„Ž:š“āŸ¶(šµ Ɨ š¶) ∧ š¹ = (š‘ƒ ∘ ā„Ž) ∧ šŗ = (š‘„ ∘ ā„Ž))) ∧ š‘§ ∈ š“) → (š¹ā€˜š‘§) = (((1st ↾ (šµ Ɨ š¶)) ∘ ā„Ž)ā€˜š‘§))
32 simpr1 1003 . . . . . . . . . 10 (((š“ ∈ š· ∧ š¹:š“āŸ¶šµ ∧ šŗ:š“āŸ¶š¶) ∧ (ā„Ž:š“āŸ¶(šµ Ɨ š¶) ∧ š¹ = (š‘ƒ ∘ ā„Ž) ∧ šŗ = (š‘„ ∘ ā„Ž))) → ā„Ž:š“āŸ¶(šµ Ɨ š¶))
33 fvco3 5590 . . . . . . . . . 10 ((ā„Ž:š“āŸ¶(šµ Ɨ š¶) ∧ š‘§ ∈ š“) → (((1st ↾ (šµ Ɨ š¶)) ∘ ā„Ž)ā€˜š‘§) = ((1st ↾ (šµ Ɨ š¶))ā€˜(ā„Žā€˜š‘§)))
3432, 33sylan 283 . . . . . . . . 9 ((((š“ ∈ š· ∧ š¹:š“āŸ¶šµ ∧ šŗ:š“āŸ¶š¶) ∧ (ā„Ž:š“āŸ¶(šµ Ɨ š¶) ∧ š¹ = (š‘ƒ ∘ ā„Ž) ∧ šŗ = (š‘„ ∘ ā„Ž))) ∧ š‘§ ∈ š“) → (((1st ↾ (šµ Ɨ š¶)) ∘ ā„Ž)ā€˜š‘§) = ((1st ↾ (šµ Ɨ š¶))ā€˜(ā„Žā€˜š‘§)))
35213ad2antl1 1159 . . . . . . . . . . 11 (((ā„Ž:š“āŸ¶(šµ Ɨ š¶) ∧ š¹ = (š‘ƒ ∘ ā„Ž) ∧ šŗ = (š‘„ ∘ ā„Ž)) ∧ š‘§ ∈ š“) → (ā„Žā€˜š‘§) ∈ (šµ Ɨ š¶))
3635adantll 476 . . . . . . . . . 10 ((((š“ ∈ š· ∧ š¹:š“āŸ¶šµ ∧ šŗ:š“āŸ¶š¶) ∧ (ā„Ž:š“āŸ¶(šµ Ɨ š¶) ∧ š¹ = (š‘ƒ ∘ ā„Ž) ∧ šŗ = (š‘„ ∘ ā„Ž))) ∧ š‘§ ∈ š“) → (ā„Žā€˜š‘§) ∈ (šµ Ɨ š¶))
3736fvresd 5542 . . . . . . . . 9 ((((š“ ∈ š· ∧ š¹:š“āŸ¶šµ ∧ šŗ:š“āŸ¶š¶) ∧ (ā„Ž:š“āŸ¶(šµ Ɨ š¶) ∧ š¹ = (š‘ƒ ∘ ā„Ž) ∧ šŗ = (š‘„ ∘ ā„Ž))) ∧ š‘§ ∈ š“) → ((1st ↾ (šµ Ɨ š¶))ā€˜(ā„Žā€˜š‘§)) = (1st ā€˜(ā„Žā€˜š‘§)))
3831, 34, 373eqtrrd 2215 . . . . . . . 8 ((((š“ ∈ š· ∧ š¹:š“āŸ¶šµ ∧ šŗ:š“āŸ¶š¶) ∧ (ā„Ž:š“āŸ¶(šµ Ɨ š¶) ∧ š¹ = (š‘ƒ ∘ ā„Ž) ∧ šŗ = (š‘„ ∘ ā„Ž))) ∧ š‘§ ∈ š“) → (1st ā€˜(ā„Žā€˜š‘§)) = (š¹ā€˜š‘§))
39 fveq1 5516 . . . . . . . . . . . 12 (šŗ = (š‘„ ∘ ā„Ž) → (šŗā€˜š‘§) = ((š‘„ ∘ ā„Ž)ā€˜š‘§))
40 upxp.2 . . . . . . . . . . . . . 14 š‘„ = (2nd ↾ (šµ Ɨ š¶))
4140coeq1i 4788 . . . . . . . . . . . . 13 (š‘„ ∘ ā„Ž) = ((2nd ↾ (šµ Ɨ š¶)) ∘ ā„Ž)
4241fveq1i 5518 . . . . . . . . . . . 12 ((š‘„ ∘ ā„Ž)ā€˜š‘§) = (((2nd ↾ (šµ Ɨ š¶)) ∘ ā„Ž)ā€˜š‘§)
4339, 42eqtrdi 2226 . . . . . . . . . . 11 (šŗ = (š‘„ ∘ ā„Ž) → (šŗā€˜š‘§) = (((2nd ↾ (šµ Ɨ š¶)) ∘ ā„Ž)ā€˜š‘§))
44433ad2ant3 1020 . . . . . . . . . 10 ((ā„Ž:š“āŸ¶(šµ Ɨ š¶) ∧ š¹ = (š‘ƒ ∘ ā„Ž) ∧ šŗ = (š‘„ ∘ ā„Ž)) → (šŗā€˜š‘§) = (((2nd ↾ (šµ Ɨ š¶)) ∘ ā„Ž)ā€˜š‘§))
4544ad2antlr 489 . . . . . . . . 9 ((((š“ ∈ š· ∧ š¹:š“āŸ¶šµ ∧ šŗ:š“āŸ¶š¶) ∧ (ā„Ž:š“āŸ¶(šµ Ɨ š¶) ∧ š¹ = (š‘ƒ ∘ ā„Ž) ∧ šŗ = (š‘„ ∘ ā„Ž))) ∧ š‘§ ∈ š“) → (šŗā€˜š‘§) = (((2nd ↾ (šµ Ɨ š¶)) ∘ ā„Ž)ā€˜š‘§))
46 fvco3 5590 . . . . . . . . . 10 ((ā„Ž:š“āŸ¶(šµ Ɨ š¶) ∧ š‘§ ∈ š“) → (((2nd ↾ (šµ Ɨ š¶)) ∘ ā„Ž)ā€˜š‘§) = ((2nd ↾ (šµ Ɨ š¶))ā€˜(ā„Žā€˜š‘§)))
4732, 46sylan 283 . . . . . . . . 9 ((((š“ ∈ š· ∧ š¹:š“āŸ¶šµ ∧ šŗ:š“āŸ¶š¶) ∧ (ā„Ž:š“āŸ¶(šµ Ɨ š¶) ∧ š¹ = (š‘ƒ ∘ ā„Ž) ∧ šŗ = (š‘„ ∘ ā„Ž))) ∧ š‘§ ∈ š“) → (((2nd ↾ (šµ Ɨ š¶)) ∘ ā„Ž)ā€˜š‘§) = ((2nd ↾ (šµ Ɨ š¶))ā€˜(ā„Žā€˜š‘§)))
4836fvresd 5542 . . . . . . . . 9 ((((š“ ∈ š· ∧ š¹:š“āŸ¶šµ ∧ šŗ:š“āŸ¶š¶) ∧ (ā„Ž:š“āŸ¶(šµ Ɨ š¶) ∧ š¹ = (š‘ƒ ∘ ā„Ž) ∧ šŗ = (š‘„ ∘ ā„Ž))) ∧ š‘§ ∈ š“) → ((2nd ↾ (šµ Ɨ š¶))ā€˜(ā„Žā€˜š‘§)) = (2nd ā€˜(ā„Žā€˜š‘§)))
4945, 47, 483eqtrrd 2215 . . . . . . . 8 ((((š“ ∈ š· ∧ š¹:š“āŸ¶šµ ∧ šŗ:š“āŸ¶š¶) ∧ (ā„Ž:š“āŸ¶(šµ Ɨ š¶) ∧ š¹ = (š‘ƒ ∘ ā„Ž) ∧ šŗ = (š‘„ ∘ ā„Ž))) ∧ š‘§ ∈ š“) → (2nd ā€˜(ā„Žā€˜š‘§)) = (šŗā€˜š‘§))
50 eqopi 6176 . . . . . . . 8 (((ā„Žā€˜š‘§) ∈ (V Ɨ V) ∧ ((1st ā€˜(ā„Žā€˜š‘§)) = (š¹ā€˜š‘§) ∧ (2nd ā€˜(ā„Žā€˜š‘§)) = (šŗā€˜š‘§))) → (ā„Žā€˜š‘§) = ⟨(š¹ā€˜š‘§), (šŗā€˜š‘§)⟩)
5124, 38, 49, 50syl12anc 1236 . . . . . . 7 ((((š“ ∈ š· ∧ š¹:š“āŸ¶šµ ∧ šŗ:š“āŸ¶š¶) ∧ (ā„Ž:š“āŸ¶(šµ Ɨ š¶) ∧ š¹ = (š‘ƒ ∘ ā„Ž) ∧ šŗ = (š‘„ ∘ ā„Ž))) ∧ š‘§ ∈ š“) → (ā„Žā€˜š‘§) = ⟨(š¹ā€˜š‘§), (šŗā€˜š‘§)⟩)
52 fveq2 5517 . . . . . . . . 9 (š‘„ = š‘§ → (š¹ā€˜š‘„) = (š¹ā€˜š‘§))
53 fveq2 5517 . . . . . . . . 9 (š‘„ = š‘§ → (šŗā€˜š‘„) = (šŗā€˜š‘§))
5452, 53opeq12d 3788 . . . . . . . 8 (š‘„ = š‘§ → ⟨(š¹ā€˜š‘„), (šŗā€˜š‘„)⟩ = ⟨(š¹ā€˜š‘§), (šŗā€˜š‘§)⟩)
55 simpr 110 . . . . . . . 8 ((((š“ ∈ š· ∧ š¹:š“āŸ¶šµ ∧ šŗ:š“āŸ¶š¶) ∧ (ā„Ž:š“āŸ¶(šµ Ɨ š¶) ∧ š¹ = (š‘ƒ ∘ ā„Ž) ∧ šŗ = (š‘„ ∘ ā„Ž))) ∧ š‘§ ∈ š“) → š‘§ ∈ š“)
5651, 36eqeltrrd 2255 . . . . . . . 8 ((((š“ ∈ š· ∧ š¹:š“āŸ¶šµ ∧ šŗ:š“āŸ¶š¶) ∧ (ā„Ž:š“āŸ¶(šµ Ɨ š¶) ∧ š¹ = (š‘ƒ ∘ ā„Ž) ∧ šŗ = (š‘„ ∘ ā„Ž))) ∧ š‘§ ∈ š“) → ⟨(š¹ā€˜š‘§), (šŗā€˜š‘§)⟩ ∈ (šµ Ɨ š¶))
5715, 54, 55, 56fvmptd3 5612 . . . . . . 7 ((((š“ ∈ š· ∧ š¹:š“āŸ¶šµ ∧ šŗ:š“āŸ¶š¶) ∧ (ā„Ž:š“āŸ¶(šµ Ɨ š¶) ∧ š¹ = (š‘ƒ ∘ ā„Ž) ∧ šŗ = (š‘„ ∘ ā„Ž))) ∧ š‘§ ∈ š“) → ((š‘„ ∈ š“ ↦ ⟨(š¹ā€˜š‘„), (šŗā€˜š‘„)⟩)ā€˜š‘§) = ⟨(š¹ā€˜š‘§), (šŗā€˜š‘§)⟩)
5851, 57eqtr4d 2213 . . . . . 6 ((((š“ ∈ š· ∧ š¹:š“āŸ¶šµ ∧ šŗ:š“āŸ¶š¶) ∧ (ā„Ž:š“āŸ¶(šµ Ɨ š¶) ∧ š¹ = (š‘ƒ ∘ ā„Ž) ∧ šŗ = (š‘„ ∘ ā„Ž))) ∧ š‘§ ∈ š“) → (ā„Žā€˜š‘§) = ((š‘„ ∈ š“ ↦ ⟨(š¹ā€˜š‘„), (šŗā€˜š‘„)⟩)ā€˜š‘§))
597, 19, 58eqfnfvd 5619 . . . . 5 (((š“ ∈ š· ∧ š¹:š“āŸ¶šµ ∧ šŗ:š“āŸ¶š¶) ∧ (ā„Ž:š“āŸ¶(šµ Ɨ š¶) ∧ š¹ = (š‘ƒ ∘ ā„Ž) ∧ šŗ = (š‘„ ∘ ā„Ž))) → ā„Ž = (š‘„ ∈ š“ ↦ ⟨(š¹ā€˜š‘„), (šŗā€˜š‘„)⟩))
6059ex 115 . . . 4 ((š“ ∈ š· ∧ š¹:š“āŸ¶šµ ∧ šŗ:š“āŸ¶š¶) → ((ā„Ž:š“āŸ¶(šµ Ɨ š¶) ∧ š¹ = (š‘ƒ ∘ ā„Ž) ∧ šŗ = (š‘„ ∘ ā„Ž)) → ā„Ž = (š‘„ ∈ š“ ↦ ⟨(š¹ā€˜š‘„), (šŗā€˜š‘„)⟩)))
61 ffn 5367 . . . . . . . . 9 (š¹:š“āŸ¶šµ → š¹ Fn š“)
62613ad2ant2 1019 . . . . . . . 8 ((š“ ∈ š· ∧ š¹:š“āŸ¶šµ ∧ šŗ:š“āŸ¶š¶) → š¹ Fn š“)
63 fo1st 6161 . . . . . . . . . . 11 1st :V–onto→V
64 fofn 5442 . . . . . . . . . . 11 (1st :V–onto→V → 1st Fn V)
6563, 64ax-mp 5 . . . . . . . . . 10 1st Fn V
66 ssv 3179 . . . . . . . . . 10 (šµ Ɨ š¶) āŠ† V
67 fnssres 5331 . . . . . . . . . 10 ((1st Fn V ∧ (šµ Ɨ š¶) āŠ† V) → (1st ↾ (šµ Ɨ š¶)) Fn (šµ Ɨ š¶))
6865, 66, 67mp2an 426 . . . . . . . . 9 (1st ↾ (šµ Ɨ š¶)) Fn (šµ Ɨ š¶)
6917frnd 5377 . . . . . . . . 9 ((š“ ∈ š· ∧ š¹:š“āŸ¶šµ ∧ šŗ:š“āŸ¶š¶) → ran (š‘„ ∈ š“ ↦ ⟨(š¹ā€˜š‘„), (šŗā€˜š‘„)⟩) āŠ† (šµ Ɨ š¶))
70 fnco 5326 . . . . . . . . 9 (((1st ↾ (šµ Ɨ š¶)) Fn (šµ Ɨ š¶) ∧ (š‘„ ∈ š“ ↦ ⟨(š¹ā€˜š‘„), (šŗā€˜š‘„)⟩) Fn š“ ∧ ran (š‘„ ∈ š“ ↦ ⟨(š¹ā€˜š‘„), (šŗā€˜š‘„)⟩) āŠ† (šµ Ɨ š¶)) → ((1st ↾ (šµ Ɨ š¶)) ∘ (š‘„ ∈ š“ ↦ ⟨(š¹ā€˜š‘„), (šŗā€˜š‘„)⟩)) Fn š“)
7168, 18, 69, 70mp3an2i 1342 . . . . . . . 8 ((š“ ∈ š· ∧ š¹:š“āŸ¶šµ ∧ šŗ:š“āŸ¶š¶) → ((1st ↾ (šµ Ɨ š¶)) ∘ (š‘„ ∈ š“ ↦ ⟨(š¹ā€˜š‘„), (šŗā€˜š‘„)⟩)) Fn š“)
72 fvco3 5590 . . . . . . . . . 10 (((š‘„ ∈ š“ ↦ ⟨(š¹ā€˜š‘„), (šŗā€˜š‘„)⟩):š“āŸ¶(šµ Ɨ š¶) ∧ š‘§ ∈ š“) → (((1st ↾ (šµ Ɨ š¶)) ∘ (š‘„ ∈ š“ ↦ ⟨(š¹ā€˜š‘„), (šŗā€˜š‘„)⟩))ā€˜š‘§) = ((1st ↾ (šµ Ɨ š¶))ā€˜((š‘„ ∈ š“ ↦ ⟨(š¹ā€˜š‘„), (šŗā€˜š‘„)⟩)ā€˜š‘§)))
7317, 72sylan 283 . . . . . . . . 9 (((š“ ∈ š· ∧ š¹:š“āŸ¶šµ ∧ šŗ:š“āŸ¶š¶) ∧ š‘§ ∈ š“) → (((1st ↾ (šµ Ɨ š¶)) ∘ (š‘„ ∈ š“ ↦ ⟨(š¹ā€˜š‘„), (šŗā€˜š‘„)⟩))ā€˜š‘§) = ((1st ↾ (šµ Ɨ š¶))ā€˜((š‘„ ∈ š“ ↦ ⟨(š¹ā€˜š‘„), (šŗā€˜š‘„)⟩)ā€˜š‘§)))
74 simpr 110 . . . . . . . . . . 11 (((š“ ∈ š· ∧ š¹:š“āŸ¶šµ ∧ šŗ:š“āŸ¶š¶) ∧ š‘§ ∈ š“) → š‘§ ∈ š“)
75 simpl2 1001 . . . . . . . . . . . . 13 (((š“ ∈ š· ∧ š¹:š“āŸ¶šµ ∧ šŗ:š“āŸ¶š¶) ∧ š‘§ ∈ š“) → š¹:š“āŸ¶šµ)
7675, 74ffvelcdmd 5655 . . . . . . . . . . . 12 (((š“ ∈ š· ∧ š¹:š“āŸ¶šµ ∧ šŗ:š“āŸ¶š¶) ∧ š‘§ ∈ š“) → (š¹ā€˜š‘§) ∈ šµ)
77 simpl3 1002 . . . . . . . . . . . . 13 (((š“ ∈ š· ∧ š¹:š“āŸ¶šµ ∧ šŗ:š“āŸ¶š¶) ∧ š‘§ ∈ š“) → šŗ:š“āŸ¶š¶)
7877, 74ffvelcdmd 5655 . . . . . . . . . . . 12 (((š“ ∈ š· ∧ š¹:š“āŸ¶šµ ∧ šŗ:š“āŸ¶š¶) ∧ š‘§ ∈ š“) → (šŗā€˜š‘§) ∈ š¶)
7976, 78opelxpd 4661 . . . . . . . . . . 11 (((š“ ∈ š· ∧ š¹:š“āŸ¶šµ ∧ šŗ:š“āŸ¶š¶) ∧ š‘§ ∈ š“) → ⟨(š¹ā€˜š‘§), (šŗā€˜š‘§)⟩ ∈ (šµ Ɨ š¶))
8015, 54, 74, 79fvmptd3 5612 . . . . . . . . . 10 (((š“ ∈ š· ∧ š¹:š“āŸ¶šµ ∧ šŗ:š“āŸ¶š¶) ∧ š‘§ ∈ š“) → ((š‘„ ∈ š“ ↦ ⟨(š¹ā€˜š‘„), (šŗā€˜š‘„)⟩)ā€˜š‘§) = ⟨(š¹ā€˜š‘§), (šŗā€˜š‘§)⟩)
8180fveq2d 5521 . . . . . . . . 9 (((š“ ∈ š· ∧ š¹:š“āŸ¶šµ ∧ šŗ:š“āŸ¶š¶) ∧ š‘§ ∈ š“) → ((1st ↾ (šµ Ɨ š¶))ā€˜((š‘„ ∈ š“ ↦ ⟨(š¹ā€˜š‘„), (šŗā€˜š‘„)⟩)ā€˜š‘§)) = ((1st ↾ (šµ Ɨ š¶))ā€˜āŸØ(š¹ā€˜š‘§), (šŗā€˜š‘§)⟩))
82 ffvelcdm 5652 . . . . . . . . . . . . . 14 ((š¹:š“āŸ¶šµ ∧ š‘§ ∈ š“) → (š¹ā€˜š‘§) ∈ šµ)
83 ffvelcdm 5652 . . . . . . . . . . . . . 14 ((šŗ:š“āŸ¶š¶ ∧ š‘§ ∈ š“) → (šŗā€˜š‘§) ∈ š¶)
84 opelxpi 4660 . . . . . . . . . . . . . 14 (((š¹ā€˜š‘§) ∈ šµ ∧ (šŗā€˜š‘§) ∈ š¶) → ⟨(š¹ā€˜š‘§), (šŗā€˜š‘§)⟩ ∈ (šµ Ɨ š¶))
8582, 83, 84syl2an 289 . . . . . . . . . . . . 13 (((š¹:š“āŸ¶šµ ∧ š‘§ ∈ š“) ∧ (šŗ:š“āŸ¶š¶ ∧ š‘§ ∈ š“)) → ⟨(š¹ā€˜š‘§), (šŗā€˜š‘§)⟩ ∈ (šµ Ɨ š¶))
8685anandirs 593 . . . . . . . . . . . 12 (((š¹:š“āŸ¶šµ ∧ šŗ:š“āŸ¶š¶) ∧ š‘§ ∈ š“) → ⟨(š¹ā€˜š‘§), (šŗā€˜š‘§)⟩ ∈ (šµ Ɨ š¶))
87863adantl1 1153 . . . . . . . . . . 11 (((š“ ∈ š· ∧ š¹:š“āŸ¶šµ ∧ šŗ:š“āŸ¶š¶) ∧ š‘§ ∈ š“) → ⟨(š¹ā€˜š‘§), (šŗā€˜š‘§)⟩ ∈ (šµ Ɨ š¶))
8887fvresd 5542 . . . . . . . . . 10 (((š“ ∈ š· ∧ š¹:š“āŸ¶šµ ∧ šŗ:š“āŸ¶š¶) ∧ š‘§ ∈ š“) → ((1st ↾ (šµ Ɨ š¶))ā€˜āŸØ(š¹ā€˜š‘§), (šŗā€˜š‘§)⟩) = (1st ā€˜āŸØ(š¹ā€˜š‘§), (šŗā€˜š‘§)⟩))
89 op1stg 6154 . . . . . . . . . . 11 (((š¹ā€˜š‘§) ∈ šµ ∧ (šŗā€˜š‘§) ∈ š¶) → (1st ā€˜āŸØ(š¹ā€˜š‘§), (šŗā€˜š‘§)⟩) = (š¹ā€˜š‘§))
9076, 78, 89syl2anc 411 . . . . . . . . . 10 (((š“ ∈ š· ∧ š¹:š“āŸ¶šµ ∧ šŗ:š“āŸ¶š¶) ∧ š‘§ ∈ š“) → (1st ā€˜āŸØ(š¹ā€˜š‘§), (šŗā€˜š‘§)⟩) = (š¹ā€˜š‘§))
9188, 90eqtrd 2210 . . . . . . . . 9 (((š“ ∈ š· ∧ š¹:š“āŸ¶šµ ∧ šŗ:š“āŸ¶š¶) ∧ š‘§ ∈ š“) → ((1st ↾ (šµ Ɨ š¶))ā€˜āŸØ(š¹ā€˜š‘§), (šŗā€˜š‘§)⟩) = (š¹ā€˜š‘§))
9273, 81, 913eqtrrd 2215 . . . . . . . 8 (((š“ ∈ š· ∧ š¹:š“āŸ¶šµ ∧ šŗ:š“āŸ¶š¶) ∧ š‘§ ∈ š“) → (š¹ā€˜š‘§) = (((1st ↾ (šµ Ɨ š¶)) ∘ (š‘„ ∈ š“ ↦ ⟨(š¹ā€˜š‘„), (šŗā€˜š‘„)⟩))ā€˜š‘§))
9362, 71, 92eqfnfvd 5619 . . . . . . 7 ((š“ ∈ š· ∧ š¹:š“āŸ¶šµ ∧ šŗ:š“āŸ¶š¶) → š¹ = ((1st ↾ (šµ Ɨ š¶)) ∘ (š‘„ ∈ š“ ↦ ⟨(š¹ā€˜š‘„), (šŗā€˜š‘„)⟩)))
9426coeq1i 4788 . . . . . . 7 (š‘ƒ ∘ (š‘„ ∈ š“ ↦ ⟨(š¹ā€˜š‘„), (šŗā€˜š‘„)⟩)) = ((1st ↾ (šµ Ɨ š¶)) ∘ (š‘„ ∈ š“ ↦ ⟨(š¹ā€˜š‘„), (šŗā€˜š‘„)⟩))
9593, 94eqtr4di 2228 . . . . . 6 ((š“ ∈ š· ∧ š¹:š“āŸ¶šµ ∧ šŗ:š“āŸ¶š¶) → š¹ = (š‘ƒ ∘ (š‘„ ∈ š“ ↦ ⟨(š¹ā€˜š‘„), (šŗā€˜š‘„)⟩)))
96 ffn 5367 . . . . . . . . 9 (šŗ:š“āŸ¶š¶ → šŗ Fn š“)
97963ad2ant3 1020 . . . . . . . 8 ((š“ ∈ š· ∧ š¹:š“āŸ¶šµ ∧ šŗ:š“āŸ¶š¶) → šŗ Fn š“)
98 fo2nd 6162 . . . . . . . . . . 11 2nd :V–onto→V
99 fofn 5442 . . . . . . . . . . 11 (2nd :V–onto→V → 2nd Fn V)
10098, 99ax-mp 5 . . . . . . . . . 10 2nd Fn V
101 fnssres 5331 . . . . . . . . . 10 ((2nd Fn V ∧ (šµ Ɨ š¶) āŠ† V) → (2nd ↾ (šµ Ɨ š¶)) Fn (šµ Ɨ š¶))
102100, 66, 101mp2an 426 . . . . . . . . 9 (2nd ↾ (šµ Ɨ š¶)) Fn (šµ Ɨ š¶)
103 fnco 5326 . . . . . . . . 9 (((2nd ↾ (šµ Ɨ š¶)) Fn (šµ Ɨ š¶) ∧ (š‘„ ∈ š“ ↦ ⟨(š¹ā€˜š‘„), (šŗā€˜š‘„)⟩) Fn š“ ∧ ran (š‘„ ∈ š“ ↦ ⟨(š¹ā€˜š‘„), (šŗā€˜š‘„)⟩) āŠ† (šµ Ɨ š¶)) → ((2nd ↾ (šµ Ɨ š¶)) ∘ (š‘„ ∈ š“ ↦ ⟨(š¹ā€˜š‘„), (šŗā€˜š‘„)⟩)) Fn š“)
104102, 18, 69, 103mp3an2i 1342 . . . . . . . 8 ((š“ ∈ š· ∧ š¹:š“āŸ¶šµ ∧ šŗ:š“āŸ¶š¶) → ((2nd ↾ (šµ Ɨ š¶)) ∘ (š‘„ ∈ š“ ↦ ⟨(š¹ā€˜š‘„), (šŗā€˜š‘„)⟩)) Fn š“)
105 fvco3 5590 . . . . . . . . . 10 (((š‘„ ∈ š“ ↦ ⟨(š¹ā€˜š‘„), (šŗā€˜š‘„)⟩):š“āŸ¶(šµ Ɨ š¶) ∧ š‘§ ∈ š“) → (((2nd ↾ (šµ Ɨ š¶)) ∘ (š‘„ ∈ š“ ↦ ⟨(š¹ā€˜š‘„), (šŗā€˜š‘„)⟩))ā€˜š‘§) = ((2nd ↾ (šµ Ɨ š¶))ā€˜((š‘„ ∈ š“ ↦ ⟨(š¹ā€˜š‘„), (šŗā€˜š‘„)⟩)ā€˜š‘§)))
10617, 105sylan 283 . . . . . . . . 9 (((š“ ∈ š· ∧ š¹:š“āŸ¶šµ ∧ šŗ:š“āŸ¶š¶) ∧ š‘§ ∈ š“) → (((2nd ↾ (šµ Ɨ š¶)) ∘ (š‘„ ∈ š“ ↦ ⟨(š¹ā€˜š‘„), (šŗā€˜š‘„)⟩))ā€˜š‘§) = ((2nd ↾ (šµ Ɨ š¶))ā€˜((š‘„ ∈ š“ ↦ ⟨(š¹ā€˜š‘„), (šŗā€˜š‘„)⟩)ā€˜š‘§)))
10780fveq2d 5521 . . . . . . . . 9 (((š“ ∈ š· ∧ š¹:š“āŸ¶šµ ∧ šŗ:š“āŸ¶š¶) ∧ š‘§ ∈ š“) → ((2nd ↾ (šµ Ɨ š¶))ā€˜((š‘„ ∈ š“ ↦ ⟨(š¹ā€˜š‘„), (šŗā€˜š‘„)⟩)ā€˜š‘§)) = ((2nd ↾ (šµ Ɨ š¶))ā€˜āŸØ(š¹ā€˜š‘§), (šŗā€˜š‘§)⟩))
10887fvresd 5542 . . . . . . . . . 10 (((š“ ∈ š· ∧ š¹:š“āŸ¶šµ ∧ šŗ:š“āŸ¶š¶) ∧ š‘§ ∈ š“) → ((2nd ↾ (šµ Ɨ š¶))ā€˜āŸØ(š¹ā€˜š‘§), (šŗā€˜š‘§)⟩) = (2nd ā€˜āŸØ(š¹ā€˜š‘§), (šŗā€˜š‘§)⟩))
109 op2ndg 6155 . . . . . . . . . . 11 (((š¹ā€˜š‘§) ∈ šµ ∧ (šŗā€˜š‘§) ∈ š¶) → (2nd ā€˜āŸØ(š¹ā€˜š‘§), (šŗā€˜š‘§)⟩) = (šŗā€˜š‘§))
11076, 78, 109syl2anc 411 . . . . . . . . . 10 (((š“ ∈ š· ∧ š¹:š“āŸ¶šµ ∧ šŗ:š“āŸ¶š¶) ∧ š‘§ ∈ š“) → (2nd ā€˜āŸØ(š¹ā€˜š‘§), (šŗā€˜š‘§)⟩) = (šŗā€˜š‘§))
111108, 110eqtrd 2210 . . . . . . . . 9 (((š“ ∈ š· ∧ š¹:š“āŸ¶šµ ∧ šŗ:š“āŸ¶š¶) ∧ š‘§ ∈ š“) → ((2nd ↾ (šµ Ɨ š¶))ā€˜āŸØ(š¹ā€˜š‘§), (šŗā€˜š‘§)⟩) = (šŗā€˜š‘§))
112106, 107, 1113eqtrrd 2215 . . . . . . . 8 (((š“ ∈ š· ∧ š¹:š“āŸ¶šµ ∧ šŗ:š“āŸ¶š¶) ∧ š‘§ ∈ š“) → (šŗā€˜š‘§) = (((2nd ↾ (šµ Ɨ š¶)) ∘ (š‘„ ∈ š“ ↦ ⟨(š¹ā€˜š‘„), (šŗā€˜š‘„)⟩))ā€˜š‘§))
11397, 104, 112eqfnfvd 5619 . . . . . . 7 ((š“ ∈ š· ∧ š¹:š“āŸ¶šµ ∧ šŗ:š“āŸ¶š¶) → šŗ = ((2nd ↾ (šµ Ɨ š¶)) ∘ (š‘„ ∈ š“ ↦ ⟨(š¹ā€˜š‘„), (šŗā€˜š‘„)⟩)))
11440coeq1i 4788 . . . . . . 7 (š‘„ ∘ (š‘„ ∈ š“ ↦ ⟨(š¹ā€˜š‘„), (šŗā€˜š‘„)⟩)) = ((2nd ↾ (šµ Ɨ š¶)) ∘ (š‘„ ∈ š“ ↦ ⟨(š¹ā€˜š‘„), (šŗā€˜š‘„)⟩))
115113, 114eqtr4di 2228 . . . . . 6 ((š“ ∈ š· ∧ š¹:š“āŸ¶šµ ∧ šŗ:š“āŸ¶š¶) → šŗ = (š‘„ ∘ (š‘„ ∈ š“ ↦ ⟨(š¹ā€˜š‘„), (šŗā€˜š‘„)⟩)))
11617, 95, 1153jca 1177 . . . . 5 ((š“ ∈ š· ∧ š¹:š“āŸ¶šµ ∧ šŗ:š“āŸ¶š¶) → ((š‘„ ∈ š“ ↦ ⟨(š¹ā€˜š‘„), (šŗā€˜š‘„)⟩):š“āŸ¶(šµ Ɨ š¶) ∧ š¹ = (š‘ƒ ∘ (š‘„ ∈ š“ ↦ ⟨(š¹ā€˜š‘„), (šŗā€˜š‘„)⟩)) ∧ šŗ = (š‘„ ∘ (š‘„ ∈ š“ ↦ ⟨(š¹ā€˜š‘„), (šŗā€˜š‘„)⟩))))
117 feq1 5350 . . . . . 6 (ā„Ž = (š‘„ ∈ š“ ↦ ⟨(š¹ā€˜š‘„), (šŗā€˜š‘„)⟩) → (ā„Ž:š“āŸ¶(šµ Ɨ š¶) ↔ (š‘„ ∈ š“ ↦ ⟨(š¹ā€˜š‘„), (šŗā€˜š‘„)⟩):š“āŸ¶(šµ Ɨ š¶)))
118 coeq2 4787 . . . . . . 7 (ā„Ž = (š‘„ ∈ š“ ↦ ⟨(š¹ā€˜š‘„), (šŗā€˜š‘„)⟩) → (š‘ƒ ∘ ā„Ž) = (š‘ƒ ∘ (š‘„ ∈ š“ ↦ ⟨(š¹ā€˜š‘„), (šŗā€˜š‘„)⟩)))
119118eqeq2d 2189 . . . . . 6 (ā„Ž = (š‘„ ∈ š“ ↦ ⟨(š¹ā€˜š‘„), (šŗā€˜š‘„)⟩) → (š¹ = (š‘ƒ ∘ ā„Ž) ↔ š¹ = (š‘ƒ ∘ (š‘„ ∈ š“ ↦ ⟨(š¹ā€˜š‘„), (šŗā€˜š‘„)⟩))))
120 coeq2 4787 . . . . . . 7 (ā„Ž = (š‘„ ∈ š“ ↦ ⟨(š¹ā€˜š‘„), (šŗā€˜š‘„)⟩) → (š‘„ ∘ ā„Ž) = (š‘„ ∘ (š‘„ ∈ š“ ↦ ⟨(š¹ā€˜š‘„), (šŗā€˜š‘„)⟩)))
121120eqeq2d 2189 . . . . . 6 (ā„Ž = (š‘„ ∈ š“ ↦ ⟨(š¹ā€˜š‘„), (šŗā€˜š‘„)⟩) → (šŗ = (š‘„ ∘ ā„Ž) ↔ šŗ = (š‘„ ∘ (š‘„ ∈ š“ ↦ ⟨(š¹ā€˜š‘„), (šŗā€˜š‘„)⟩))))
122117, 119, 1213anbi123d 1312 . . . . 5 (ā„Ž = (š‘„ ∈ š“ ↦ ⟨(š¹ā€˜š‘„), (šŗā€˜š‘„)⟩) → ((ā„Ž:š“āŸ¶(šµ Ɨ š¶) ∧ š¹ = (š‘ƒ ∘ ā„Ž) ∧ šŗ = (š‘„ ∘ ā„Ž)) ↔ ((š‘„ ∈ š“ ↦ ⟨(š¹ā€˜š‘„), (šŗā€˜š‘„)⟩):š“āŸ¶(šµ Ɨ š¶) ∧ š¹ = (š‘ƒ ∘ (š‘„ ∈ š“ ↦ ⟨(š¹ā€˜š‘„), (šŗā€˜š‘„)⟩)) ∧ šŗ = (š‘„ ∘ (š‘„ ∈ š“ ↦ ⟨(š¹ā€˜š‘„), (šŗā€˜š‘„)⟩)))))
123116, 122syl5ibrcom 157 . . . 4 ((š“ ∈ š· ∧ š¹:š“āŸ¶šµ ∧ šŗ:š“āŸ¶š¶) → (ā„Ž = (š‘„ ∈ š“ ↦ ⟨(š¹ā€˜š‘„), (šŗā€˜š‘„)⟩) → (ā„Ž:š“āŸ¶(šµ Ɨ š¶) ∧ š¹ = (š‘ƒ ∘ ā„Ž) ∧ šŗ = (š‘„ ∘ ā„Ž))))
12460, 123impbid 129 . . 3 ((š“ ∈ š· ∧ š¹:š“āŸ¶šµ ∧ šŗ:š“āŸ¶š¶) → ((ā„Ž:š“āŸ¶(šµ Ɨ š¶) ∧ š¹ = (š‘ƒ ∘ ā„Ž) ∧ šŗ = (š‘„ ∘ ā„Ž)) ↔ ā„Ž = (š‘„ ∈ š“ ↦ ⟨(š¹ā€˜š‘„), (šŗā€˜š‘„)⟩)))
125124eubidv 2034 . 2 ((š“ ∈ š· ∧ š¹:š“āŸ¶šµ ∧ šŗ:š“āŸ¶š¶) → (∃!ā„Ž(ā„Ž:š“āŸ¶(šµ Ɨ š¶) ∧ š¹ = (š‘ƒ ∘ ā„Ž) ∧ šŗ = (š‘„ ∘ ā„Ž)) ↔ ∃!ā„Ž ā„Ž = (š‘„ ∈ š“ ↦ ⟨(š¹ā€˜š‘„), (šŗā€˜š‘„)⟩)))
1264, 125mpbird 167 1 ((š“ ∈ š· ∧ š¹:š“āŸ¶šµ ∧ šŗ:š“āŸ¶š¶) → ∃!ā„Ž(ā„Ž:š“āŸ¶(šµ Ɨ š¶) ∧ š¹ = (š‘ƒ ∘ ā„Ž) ∧ šŗ = (š‘„ ∘ ā„Ž)))
Colors of variables: wff set class
Syntax hints:   → wi 4   ∧ wa 104   ∧ w3a 978   = wceq 1353  āˆƒ!weu 2026   ∈ wcel 2148  āˆ€wral 2455  Vcvv 2739   āŠ† wss 3131  āŸØcop 3597   ↦ cmpt 4066   Ɨ cxp 4626  ran crn 4629   ↾ cres 4630   ∘ ccom 4632   Fn wfn 5213  āŸ¶wf 5214  ā€“onto→wfo 5216  ā€˜cfv 5218  1st c1st 6142  2nd c2nd 6143
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-13 2150  ax-14 2151  ax-ext 2159  ax-coll 4120  ax-sep 4123  ax-pow 4176  ax-pr 4211  ax-un 4435
This theorem depends on definitions:  df-bi 117  df-3an 980  df-tru 1356  df-nf 1461  df-sb 1763  df-eu 2029  df-mo 2030  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ral 2460  df-rex 2461  df-reu 2462  df-rab 2464  df-v 2741  df-sbc 2965  df-csb 3060  df-un 3135  df-in 3137  df-ss 3144  df-pw 3579  df-sn 3600  df-pr 3601  df-op 3603  df-uni 3812  df-iun 3890  df-br 4006  df-opab 4067  df-mpt 4068  df-id 4295  df-xp 4634  df-rel 4635  df-cnv 4636  df-co 4637  df-dm 4638  df-rn 4639  df-res 4640  df-ima 4641  df-iota 5180  df-fun 5220  df-fn 5221  df-f 5222  df-f1 5223  df-fo 5224  df-f1o 5225  df-fv 5226  df-1st 6144  df-2nd 6145
This theorem is referenced by:  uptx  13935  txcn  13936
  Copyright terms: Public domain W3C validator