**Description:** Definition of reflexive-transitive closure as a standard closure.
(Contributed by RP, 1-Nov-2020)

Ref | Expression | ||
---|---|---|---|

Assertion | dfrtrcl5 | ⊢ t* = ( 𝑥 ∈ V ↦ ∩ { 𝑦 ∣ ( 𝑥 ⊆ 𝑦 ∧ ( ( I ↾ ( dom 𝑦 ∪ ran 𝑦 ) ) ⊆ 𝑦 ∧ ( 𝑦 ∘ 𝑦 ) ⊆ 𝑦 ) ) } ) |

Step | Hyp | Ref | Expression |
---|---|---|---|

1 | df-rtrcl | ⊢ t* = ( 𝑥 ∈ V ↦ ∩ { 𝑧 ∣ ( ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ⊆ 𝑧 ∧ 𝑥 ⊆ 𝑧 ∧ ( 𝑧 ∘ 𝑧 ) ⊆ 𝑧 ) } ) | |

2 | ancom | ⊢ ( ( ( I ↾ ( dom 𝑦 ∪ ran 𝑦 ) ) ⊆ 𝑦 ∧ ( 𝑦 ∘ 𝑦 ) ⊆ 𝑦 ) ↔ ( ( 𝑦 ∘ 𝑦 ) ⊆ 𝑦 ∧ ( I ↾ ( dom 𝑦 ∪ ran 𝑦 ) ) ⊆ 𝑦 ) ) | |

3 | 2 | anbi2i | ⊢ ( ( 𝑥 ⊆ 𝑦 ∧ ( ( I ↾ ( dom 𝑦 ∪ ran 𝑦 ) ) ⊆ 𝑦 ∧ ( 𝑦 ∘ 𝑦 ) ⊆ 𝑦 ) ) ↔ ( 𝑥 ⊆ 𝑦 ∧ ( ( 𝑦 ∘ 𝑦 ) ⊆ 𝑦 ∧ ( I ↾ ( dom 𝑦 ∪ ran 𝑦 ) ) ⊆ 𝑦 ) ) ) |

4 | 3 | abbii | ⊢ { 𝑦 ∣ ( 𝑥 ⊆ 𝑦 ∧ ( ( I ↾ ( dom 𝑦 ∪ ran 𝑦 ) ) ⊆ 𝑦 ∧ ( 𝑦 ∘ 𝑦 ) ⊆ 𝑦 ) ) } = { 𝑦 ∣ ( 𝑥 ⊆ 𝑦 ∧ ( ( 𝑦 ∘ 𝑦 ) ⊆ 𝑦 ∧ ( I ↾ ( dom 𝑦 ∪ ran 𝑦 ) ) ⊆ 𝑦 ) ) } |

5 | 4 | inteqi | ⊢ ∩ { 𝑦 ∣ ( 𝑥 ⊆ 𝑦 ∧ ( ( I ↾ ( dom 𝑦 ∪ ran 𝑦 ) ) ⊆ 𝑦 ∧ ( 𝑦 ∘ 𝑦 ) ⊆ 𝑦 ) ) } = ∩ { 𝑦 ∣ ( 𝑥 ⊆ 𝑦 ∧ ( ( 𝑦 ∘ 𝑦 ) ⊆ 𝑦 ∧ ( I ↾ ( dom 𝑦 ∪ ran 𝑦 ) ) ⊆ 𝑦 ) ) } |

6 | 5 | mpteq2i | ⊢ ( 𝑥 ∈ V ↦ ∩ { 𝑦 ∣ ( 𝑥 ⊆ 𝑦 ∧ ( ( I ↾ ( dom 𝑦 ∪ ran 𝑦 ) ) ⊆ 𝑦 ∧ ( 𝑦 ∘ 𝑦 ) ⊆ 𝑦 ) ) } ) = ( 𝑥 ∈ V ↦ ∩ { 𝑦 ∣ ( 𝑥 ⊆ 𝑦 ∧ ( ( 𝑦 ∘ 𝑦 ) ⊆ 𝑦 ∧ ( I ↾ ( dom 𝑦 ∪ ran 𝑦 ) ) ⊆ 𝑦 ) ) } ) |

7 | vex | ⊢ 𝑥 ∈ V | |

8 | 7 | rtrclexi | ⊢ ∩ { 𝑦 ∣ ( 𝑥 ⊆ 𝑦 ∧ ( ( 𝑦 ∘ 𝑦 ) ⊆ 𝑦 ∧ ( I ↾ ( dom 𝑦 ∪ ran 𝑦 ) ) ⊆ 𝑦 ) ) } ∈ V |

9 | 8 | a1i | ⊢ ( 𝑥 ∈ V → ∩ { 𝑦 ∣ ( 𝑥 ⊆ 𝑦 ∧ ( ( 𝑦 ∘ 𝑦 ) ⊆ 𝑦 ∧ ( I ↾ ( dom 𝑦 ∪ ran 𝑦 ) ) ⊆ 𝑦 ) ) } ∈ V ) |

10 | dmexg | ⊢ ( 𝑥 ∈ V → dom 𝑥 ∈ V ) | |

11 | rnexg | ⊢ ( 𝑥 ∈ V → ran 𝑥 ∈ V ) | |

12 | unexg | ⊢ ( ( dom 𝑥 ∈ V ∧ ran 𝑥 ∈ V ) → ( dom 𝑥 ∪ ran 𝑥 ) ∈ V ) | |

13 | 10 11 12 | syl2anc | ⊢ ( 𝑥 ∈ V → ( dom 𝑥 ∪ ran 𝑥 ) ∈ V ) |

14 | resiexg | ⊢ ( ( dom 𝑥 ∪ ran 𝑥 ) ∈ V → ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ∈ V ) | |

15 | 7 13 14 | mp2b | ⊢ ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ∈ V |

16 | 7 15 | unex | ⊢ ( 𝑥 ∪ ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ) ∈ V |

17 | 16 | trclexi | ⊢ ∩ { 𝑧 ∣ ( ( 𝑥 ∪ ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ) ⊆ 𝑧 ∧ ( 𝑧 ∘ 𝑧 ) ⊆ 𝑧 ) } ∈ V |

18 | 17 | a1i | ⊢ ( 𝑥 ∈ V → ∩ { 𝑧 ∣ ( ( 𝑥 ∪ ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ) ⊆ 𝑧 ∧ ( 𝑧 ∘ 𝑧 ) ⊆ 𝑧 ) } ∈ V ) |

19 | simpr | ⊢ ( ( ( 𝑥 ∪ ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ) ⊆ 𝑧 ∧ ( 𝑧 ∘ 𝑧 ) ⊆ 𝑧 ) → ( 𝑧 ∘ 𝑧 ) ⊆ 𝑧 ) | |

20 | 19 | cotrintab | ⊢ ( ∩ { 𝑧 ∣ ( ( 𝑥 ∪ ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ) ⊆ 𝑧 ∧ ( 𝑧 ∘ 𝑧 ) ⊆ 𝑧 ) } ∘ ∩ { 𝑧 ∣ ( ( 𝑥 ∪ ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ) ⊆ 𝑧 ∧ ( 𝑧 ∘ 𝑧 ) ⊆ 𝑧 ) } ) ⊆ ∩ { 𝑧 ∣ ( ( 𝑥 ∪ ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ) ⊆ 𝑧 ∧ ( 𝑧 ∘ 𝑧 ) ⊆ 𝑧 ) } |

21 | 20 | a1i | ⊢ ( 𝑥 ∈ V → ( ∩ { 𝑧 ∣ ( ( 𝑥 ∪ ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ) ⊆ 𝑧 ∧ ( 𝑧 ∘ 𝑧 ) ⊆ 𝑧 ) } ∘ ∩ { 𝑧 ∣ ( ( 𝑥 ∪ ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ) ⊆ 𝑧 ∧ ( 𝑧 ∘ 𝑧 ) ⊆ 𝑧 ) } ) ⊆ ∩ { 𝑧 ∣ ( ( 𝑥 ∪ ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ) ⊆ 𝑧 ∧ ( 𝑧 ∘ 𝑧 ) ⊆ 𝑧 ) } ) |

22 | 7 | dmex | ⊢ dom 𝑥 ∈ V |

23 | 7 | rnex | ⊢ ran 𝑥 ∈ V |

24 | 12 | resiexd | ⊢ ( ( dom 𝑥 ∈ V ∧ ran 𝑥 ∈ V ) → ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ∈ V ) |

25 | 22 23 24 | mp2an | ⊢ ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ∈ V |

26 | 7 25 | unex | ⊢ ( 𝑥 ∪ ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ) ∈ V |

27 | dmtrcl | ⊢ ( ( 𝑥 ∪ ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ) ∈ V → dom ∩ { 𝑧 ∣ ( ( 𝑥 ∪ ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ) ⊆ 𝑧 ∧ ( 𝑧 ∘ 𝑧 ) ⊆ 𝑧 ) } = dom ( 𝑥 ∪ ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ) ) | |

28 | 26 27 | ax-mp | ⊢ dom ∩ { 𝑧 ∣ ( ( 𝑥 ∪ ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ) ⊆ 𝑧 ∧ ( 𝑧 ∘ 𝑧 ) ⊆ 𝑧 ) } = dom ( 𝑥 ∪ ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ) |

29 | dmun | ⊢ dom ( 𝑥 ∪ ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ) = ( dom 𝑥 ∪ dom ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ) | |

30 | dmresi | ⊢ dom ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) = ( dom 𝑥 ∪ ran 𝑥 ) | |

31 | 30 | uneq2i | ⊢ ( dom 𝑥 ∪ dom ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ) = ( dom 𝑥 ∪ ( dom 𝑥 ∪ ran 𝑥 ) ) |

32 | ssun1 | ⊢ dom 𝑥 ⊆ ( dom 𝑥 ∪ ran 𝑥 ) | |

33 | ssequn1 | ⊢ ( dom 𝑥 ⊆ ( dom 𝑥 ∪ ran 𝑥 ) ↔ ( dom 𝑥 ∪ ( dom 𝑥 ∪ ran 𝑥 ) ) = ( dom 𝑥 ∪ ran 𝑥 ) ) | |

34 | 32 33 | mpbi | ⊢ ( dom 𝑥 ∪ ( dom 𝑥 ∪ ran 𝑥 ) ) = ( dom 𝑥 ∪ ran 𝑥 ) |

35 | 29 31 34 | 3eqtri | ⊢ dom ( 𝑥 ∪ ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ) = ( dom 𝑥 ∪ ran 𝑥 ) |

36 | 28 35 | eqtri | ⊢ dom ∩ { 𝑧 ∣ ( ( 𝑥 ∪ ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ) ⊆ 𝑧 ∧ ( 𝑧 ∘ 𝑧 ) ⊆ 𝑧 ) } = ( dom 𝑥 ∪ ran 𝑥 ) |

37 | rntrcl | ⊢ ( ( 𝑥 ∪ ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ) ∈ V → ran ∩ { 𝑧 ∣ ( ( 𝑥 ∪ ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ) ⊆ 𝑧 ∧ ( 𝑧 ∘ 𝑧 ) ⊆ 𝑧 ) } = ran ( 𝑥 ∪ ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ) ) | |

38 | 26 37 | ax-mp | ⊢ ran ∩ { 𝑧 ∣ ( ( 𝑥 ∪ ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ) ⊆ 𝑧 ∧ ( 𝑧 ∘ 𝑧 ) ⊆ 𝑧 ) } = ran ( 𝑥 ∪ ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ) |

39 | rnun | ⊢ ran ( 𝑥 ∪ ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ) = ( ran 𝑥 ∪ ran ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ) | |

40 | rnresi | ⊢ ran ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) = ( dom 𝑥 ∪ ran 𝑥 ) | |

41 | 40 | uneq2i | ⊢ ( ran 𝑥 ∪ ran ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ) = ( ran 𝑥 ∪ ( dom 𝑥 ∪ ran 𝑥 ) ) |

42 | ssun2 | ⊢ ran 𝑥 ⊆ ( dom 𝑥 ∪ ran 𝑥 ) | |

43 | ssequn1 | ⊢ ( ran 𝑥 ⊆ ( dom 𝑥 ∪ ran 𝑥 ) ↔ ( ran 𝑥 ∪ ( dom 𝑥 ∪ ran 𝑥 ) ) = ( dom 𝑥 ∪ ran 𝑥 ) ) | |

44 | 42 43 | mpbi | ⊢ ( ran 𝑥 ∪ ( dom 𝑥 ∪ ran 𝑥 ) ) = ( dom 𝑥 ∪ ran 𝑥 ) |

45 | 39 41 44 | 3eqtri | ⊢ ran ( 𝑥 ∪ ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ) = ( dom 𝑥 ∪ ran 𝑥 ) |

46 | 38 45 | eqtri | ⊢ ran ∩ { 𝑧 ∣ ( ( 𝑥 ∪ ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ) ⊆ 𝑧 ∧ ( 𝑧 ∘ 𝑧 ) ⊆ 𝑧 ) } = ( dom 𝑥 ∪ ran 𝑥 ) |

47 | 36 46 | uneq12i | ⊢ ( dom ∩ { 𝑧 ∣ ( ( 𝑥 ∪ ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ) ⊆ 𝑧 ∧ ( 𝑧 ∘ 𝑧 ) ⊆ 𝑧 ) } ∪ ran ∩ { 𝑧 ∣ ( ( 𝑥 ∪ ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ) ⊆ 𝑧 ∧ ( 𝑧 ∘ 𝑧 ) ⊆ 𝑧 ) } ) = ( ( dom 𝑥 ∪ ran 𝑥 ) ∪ ( dom 𝑥 ∪ ran 𝑥 ) ) |

48 | unidm | ⊢ ( ( dom 𝑥 ∪ ran 𝑥 ) ∪ ( dom 𝑥 ∪ ran 𝑥 ) ) = ( dom 𝑥 ∪ ran 𝑥 ) | |

49 | 47 48 | eqtri | ⊢ ( dom ∩ { 𝑧 ∣ ( ( 𝑥 ∪ ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ) ⊆ 𝑧 ∧ ( 𝑧 ∘ 𝑧 ) ⊆ 𝑧 ) } ∪ ran ∩ { 𝑧 ∣ ( ( 𝑥 ∪ ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ) ⊆ 𝑧 ∧ ( 𝑧 ∘ 𝑧 ) ⊆ 𝑧 ) } ) = ( dom 𝑥 ∪ ran 𝑥 ) |

50 | 49 | reseq2i | ⊢ ( I ↾ ( dom ∩ { 𝑧 ∣ ( ( 𝑥 ∪ ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ) ⊆ 𝑧 ∧ ( 𝑧 ∘ 𝑧 ) ⊆ 𝑧 ) } ∪ ran ∩ { 𝑧 ∣ ( ( 𝑥 ∪ ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ) ⊆ 𝑧 ∧ ( 𝑧 ∘ 𝑧 ) ⊆ 𝑧 ) } ) ) = ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) |

51 | ssun2 | ⊢ ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ⊆ ( 𝑥 ∪ ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ) | |

52 | ssmin | ⊢ ( 𝑥 ∪ ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ) ⊆ ∩ { 𝑧 ∣ ( ( 𝑥 ∪ ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ) ⊆ 𝑧 ∧ ( 𝑧 ∘ 𝑧 ) ⊆ 𝑧 ) } | |

53 | 51 52 | sstri | ⊢ ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ⊆ ∩ { 𝑧 ∣ ( ( 𝑥 ∪ ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ) ⊆ 𝑧 ∧ ( 𝑧 ∘ 𝑧 ) ⊆ 𝑧 ) } |

54 | 50 53 | eqsstri | ⊢ ( I ↾ ( dom ∩ { 𝑧 ∣ ( ( 𝑥 ∪ ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ) ⊆ 𝑧 ∧ ( 𝑧 ∘ 𝑧 ) ⊆ 𝑧 ) } ∪ ran ∩ { 𝑧 ∣ ( ( 𝑥 ∪ ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ) ⊆ 𝑧 ∧ ( 𝑧 ∘ 𝑧 ) ⊆ 𝑧 ) } ) ) ⊆ ∩ { 𝑧 ∣ ( ( 𝑥 ∪ ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ) ⊆ 𝑧 ∧ ( 𝑧 ∘ 𝑧 ) ⊆ 𝑧 ) } |

55 | 54 | a1i | ⊢ ( 𝑥 ∈ V → ( I ↾ ( dom ∩ { 𝑧 ∣ ( ( 𝑥 ∪ ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ) ⊆ 𝑧 ∧ ( 𝑧 ∘ 𝑧 ) ⊆ 𝑧 ) } ∪ ran ∩ { 𝑧 ∣ ( ( 𝑥 ∪ ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ) ⊆ 𝑧 ∧ ( 𝑧 ∘ 𝑧 ) ⊆ 𝑧 ) } ) ) ⊆ ∩ { 𝑧 ∣ ( ( 𝑥 ∪ ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ) ⊆ 𝑧 ∧ ( 𝑧 ∘ 𝑧 ) ⊆ 𝑧 ) } ) |

56 | simprl | ⊢ ( ( 𝑥 ⊆ 𝑦 ∧ ( ( 𝑦 ∘ 𝑦 ) ⊆ 𝑦 ∧ ( I ↾ ( dom 𝑦 ∪ ran 𝑦 ) ) ⊆ 𝑦 ) ) → ( 𝑦 ∘ 𝑦 ) ⊆ 𝑦 ) | |

57 | 56 | cotrintab | ⊢ ( ∩ { 𝑦 ∣ ( 𝑥 ⊆ 𝑦 ∧ ( ( 𝑦 ∘ 𝑦 ) ⊆ 𝑦 ∧ ( I ↾ ( dom 𝑦 ∪ ran 𝑦 ) ) ⊆ 𝑦 ) ) } ∘ ∩ { 𝑦 ∣ ( 𝑥 ⊆ 𝑦 ∧ ( ( 𝑦 ∘ 𝑦 ) ⊆ 𝑦 ∧ ( I ↾ ( dom 𝑦 ∪ ran 𝑦 ) ) ⊆ 𝑦 ) ) } ) ⊆ ∩ { 𝑦 ∣ ( 𝑥 ⊆ 𝑦 ∧ ( ( 𝑦 ∘ 𝑦 ) ⊆ 𝑦 ∧ ( I ↾ ( dom 𝑦 ∪ ran 𝑦 ) ) ⊆ 𝑦 ) ) } |

58 | 57 | a1i | ⊢ ( 𝑥 ∈ V → ( ∩ { 𝑦 ∣ ( 𝑥 ⊆ 𝑦 ∧ ( ( 𝑦 ∘ 𝑦 ) ⊆ 𝑦 ∧ ( I ↾ ( dom 𝑦 ∪ ran 𝑦 ) ) ⊆ 𝑦 ) ) } ∘ ∩ { 𝑦 ∣ ( 𝑥 ⊆ 𝑦 ∧ ( ( 𝑦 ∘ 𝑦 ) ⊆ 𝑦 ∧ ( I ↾ ( dom 𝑦 ∪ ran 𝑦 ) ) ⊆ 𝑦 ) ) } ) ⊆ ∩ { 𝑦 ∣ ( 𝑥 ⊆ 𝑦 ∧ ( ( 𝑦 ∘ 𝑦 ) ⊆ 𝑦 ∧ ( I ↾ ( dom 𝑦 ∪ ran 𝑦 ) ) ⊆ 𝑦 ) ) } ) |

59 | id | ⊢ ( 𝑦 = ∩ { 𝑧 ∣ ( ( 𝑥 ∪ ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ) ⊆ 𝑧 ∧ ( 𝑧 ∘ 𝑧 ) ⊆ 𝑧 ) } → 𝑦 = ∩ { 𝑧 ∣ ( ( 𝑥 ∪ ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ) ⊆ 𝑧 ∧ ( 𝑧 ∘ 𝑧 ) ⊆ 𝑧 ) } ) | |

60 | 59 59 | coeq12d | ⊢ ( 𝑦 = ∩ { 𝑧 ∣ ( ( 𝑥 ∪ ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ) ⊆ 𝑧 ∧ ( 𝑧 ∘ 𝑧 ) ⊆ 𝑧 ) } → ( 𝑦 ∘ 𝑦 ) = ( ∩ { 𝑧 ∣ ( ( 𝑥 ∪ ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ) ⊆ 𝑧 ∧ ( 𝑧 ∘ 𝑧 ) ⊆ 𝑧 ) } ∘ ∩ { 𝑧 ∣ ( ( 𝑥 ∪ ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ) ⊆ 𝑧 ∧ ( 𝑧 ∘ 𝑧 ) ⊆ 𝑧 ) } ) ) |

61 | 60 59 | sseq12d | ⊢ ( 𝑦 = ∩ { 𝑧 ∣ ( ( 𝑥 ∪ ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ) ⊆ 𝑧 ∧ ( 𝑧 ∘ 𝑧 ) ⊆ 𝑧 ) } → ( ( 𝑦 ∘ 𝑦 ) ⊆ 𝑦 ↔ ( ∩ { 𝑧 ∣ ( ( 𝑥 ∪ ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ) ⊆ 𝑧 ∧ ( 𝑧 ∘ 𝑧 ) ⊆ 𝑧 ) } ∘ ∩ { 𝑧 ∣ ( ( 𝑥 ∪ ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ) ⊆ 𝑧 ∧ ( 𝑧 ∘ 𝑧 ) ⊆ 𝑧 ) } ) ⊆ ∩ { 𝑧 ∣ ( ( 𝑥 ∪ ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ) ⊆ 𝑧 ∧ ( 𝑧 ∘ 𝑧 ) ⊆ 𝑧 ) } ) ) |

62 | dmeq | ⊢ ( 𝑦 = ∩ { 𝑧 ∣ ( ( 𝑥 ∪ ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ) ⊆ 𝑧 ∧ ( 𝑧 ∘ 𝑧 ) ⊆ 𝑧 ) } → dom 𝑦 = dom ∩ { 𝑧 ∣ ( ( 𝑥 ∪ ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ) ⊆ 𝑧 ∧ ( 𝑧 ∘ 𝑧 ) ⊆ 𝑧 ) } ) | |

63 | rneq | ⊢ ( 𝑦 = ∩ { 𝑧 ∣ ( ( 𝑥 ∪ ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ) ⊆ 𝑧 ∧ ( 𝑧 ∘ 𝑧 ) ⊆ 𝑧 ) } → ran 𝑦 = ran ∩ { 𝑧 ∣ ( ( 𝑥 ∪ ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ) ⊆ 𝑧 ∧ ( 𝑧 ∘ 𝑧 ) ⊆ 𝑧 ) } ) | |

64 | 62 63 | uneq12d | ⊢ ( 𝑦 = ∩ { 𝑧 ∣ ( ( 𝑥 ∪ ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ) ⊆ 𝑧 ∧ ( 𝑧 ∘ 𝑧 ) ⊆ 𝑧 ) } → ( dom 𝑦 ∪ ran 𝑦 ) = ( dom ∩ { 𝑧 ∣ ( ( 𝑥 ∪ ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ) ⊆ 𝑧 ∧ ( 𝑧 ∘ 𝑧 ) ⊆ 𝑧 ) } ∪ ran ∩ { 𝑧 ∣ ( ( 𝑥 ∪ ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ) ⊆ 𝑧 ∧ ( 𝑧 ∘ 𝑧 ) ⊆ 𝑧 ) } ) ) |

65 | 64 | reseq2d | ⊢ ( 𝑦 = ∩ { 𝑧 ∣ ( ( 𝑥 ∪ ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ) ⊆ 𝑧 ∧ ( 𝑧 ∘ 𝑧 ) ⊆ 𝑧 ) } → ( I ↾ ( dom 𝑦 ∪ ran 𝑦 ) ) = ( I ↾ ( dom ∩ { 𝑧 ∣ ( ( 𝑥 ∪ ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ) ⊆ 𝑧 ∧ ( 𝑧 ∘ 𝑧 ) ⊆ 𝑧 ) } ∪ ran ∩ { 𝑧 ∣ ( ( 𝑥 ∪ ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ) ⊆ 𝑧 ∧ ( 𝑧 ∘ 𝑧 ) ⊆ 𝑧 ) } ) ) ) |

66 | 65 59 | sseq12d | ⊢ ( 𝑦 = ∩ { 𝑧 ∣ ( ( 𝑥 ∪ ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ) ⊆ 𝑧 ∧ ( 𝑧 ∘ 𝑧 ) ⊆ 𝑧 ) } → ( ( I ↾ ( dom 𝑦 ∪ ran 𝑦 ) ) ⊆ 𝑦 ↔ ( I ↾ ( dom ∩ { 𝑧 ∣ ( ( 𝑥 ∪ ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ) ⊆ 𝑧 ∧ ( 𝑧 ∘ 𝑧 ) ⊆ 𝑧 ) } ∪ ran ∩ { 𝑧 ∣ ( ( 𝑥 ∪ ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ) ⊆ 𝑧 ∧ ( 𝑧 ∘ 𝑧 ) ⊆ 𝑧 ) } ) ) ⊆ ∩ { 𝑧 ∣ ( ( 𝑥 ∪ ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ) ⊆ 𝑧 ∧ ( 𝑧 ∘ 𝑧 ) ⊆ 𝑧 ) } ) ) |

67 | id | ⊢ ( 𝑧 = ∩ { 𝑦 ∣ ( 𝑥 ⊆ 𝑦 ∧ ( ( 𝑦 ∘ 𝑦 ) ⊆ 𝑦 ∧ ( I ↾ ( dom 𝑦 ∪ ran 𝑦 ) ) ⊆ 𝑦 ) ) } → 𝑧 = ∩ { 𝑦 ∣ ( 𝑥 ⊆ 𝑦 ∧ ( ( 𝑦 ∘ 𝑦 ) ⊆ 𝑦 ∧ ( I ↾ ( dom 𝑦 ∪ ran 𝑦 ) ) ⊆ 𝑦 ) ) } ) | |

68 | 67 67 | coeq12d | ⊢ ( 𝑧 = ∩ { 𝑦 ∣ ( 𝑥 ⊆ 𝑦 ∧ ( ( 𝑦 ∘ 𝑦 ) ⊆ 𝑦 ∧ ( I ↾ ( dom 𝑦 ∪ ran 𝑦 ) ) ⊆ 𝑦 ) ) } → ( 𝑧 ∘ 𝑧 ) = ( ∩ { 𝑦 ∣ ( 𝑥 ⊆ 𝑦 ∧ ( ( 𝑦 ∘ 𝑦 ) ⊆ 𝑦 ∧ ( I ↾ ( dom 𝑦 ∪ ran 𝑦 ) ) ⊆ 𝑦 ) ) } ∘ ∩ { 𝑦 ∣ ( 𝑥 ⊆ 𝑦 ∧ ( ( 𝑦 ∘ 𝑦 ) ⊆ 𝑦 ∧ ( I ↾ ( dom 𝑦 ∪ ran 𝑦 ) ) ⊆ 𝑦 ) ) } ) ) |

69 | 68 67 | sseq12d | ⊢ ( 𝑧 = ∩ { 𝑦 ∣ ( 𝑥 ⊆ 𝑦 ∧ ( ( 𝑦 ∘ 𝑦 ) ⊆ 𝑦 ∧ ( I ↾ ( dom 𝑦 ∪ ran 𝑦 ) ) ⊆ 𝑦 ) ) } → ( ( 𝑧 ∘ 𝑧 ) ⊆ 𝑧 ↔ ( ∩ { 𝑦 ∣ ( 𝑥 ⊆ 𝑦 ∧ ( ( 𝑦 ∘ 𝑦 ) ⊆ 𝑦 ∧ ( I ↾ ( dom 𝑦 ∪ ran 𝑦 ) ) ⊆ 𝑦 ) ) } ∘ ∩ { 𝑦 ∣ ( 𝑥 ⊆ 𝑦 ∧ ( ( 𝑦 ∘ 𝑦 ) ⊆ 𝑦 ∧ ( I ↾ ( dom 𝑦 ∪ ran 𝑦 ) ) ⊆ 𝑦 ) ) } ) ⊆ ∩ { 𝑦 ∣ ( 𝑥 ⊆ 𝑦 ∧ ( ( 𝑦 ∘ 𝑦 ) ⊆ 𝑦 ∧ ( I ↾ ( dom 𝑦 ∪ ran 𝑦 ) ) ⊆ 𝑦 ) ) } ) ) |

70 | 9 18 21 55 58 61 66 69 | mptrcllem | ⊢ ( 𝑥 ∈ V ↦ ∩ { 𝑦 ∣ ( 𝑥 ⊆ 𝑦 ∧ ( ( 𝑦 ∘ 𝑦 ) ⊆ 𝑦 ∧ ( I ↾ ( dom 𝑦 ∪ ran 𝑦 ) ) ⊆ 𝑦 ) ) } ) = ( 𝑥 ∈ V ↦ ∩ { 𝑧 ∣ ( ( 𝑥 ∪ ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ) ⊆ 𝑧 ∧ ( 𝑧 ∘ 𝑧 ) ⊆ 𝑧 ) } ) |

71 | df-3an | ⊢ ( ( ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ⊆ 𝑧 ∧ 𝑥 ⊆ 𝑧 ∧ ( 𝑧 ∘ 𝑧 ) ⊆ 𝑧 ) ↔ ( ( ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ⊆ 𝑧 ∧ 𝑥 ⊆ 𝑧 ) ∧ ( 𝑧 ∘ 𝑧 ) ⊆ 𝑧 ) ) | |

72 | ancom | ⊢ ( ( ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ⊆ 𝑧 ∧ 𝑥 ⊆ 𝑧 ) ↔ ( 𝑥 ⊆ 𝑧 ∧ ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ⊆ 𝑧 ) ) | |

73 | unss | ⊢ ( ( 𝑥 ⊆ 𝑧 ∧ ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ⊆ 𝑧 ) ↔ ( 𝑥 ∪ ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ) ⊆ 𝑧 ) | |

74 | 72 73 | bitri | ⊢ ( ( ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ⊆ 𝑧 ∧ 𝑥 ⊆ 𝑧 ) ↔ ( 𝑥 ∪ ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ) ⊆ 𝑧 ) |

75 | 74 | anbi1i | ⊢ ( ( ( ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ⊆ 𝑧 ∧ 𝑥 ⊆ 𝑧 ) ∧ ( 𝑧 ∘ 𝑧 ) ⊆ 𝑧 ) ↔ ( ( 𝑥 ∪ ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ) ⊆ 𝑧 ∧ ( 𝑧 ∘ 𝑧 ) ⊆ 𝑧 ) ) |

76 | 71 75 | bitr2i | ⊢ ( ( ( 𝑥 ∪ ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ) ⊆ 𝑧 ∧ ( 𝑧 ∘ 𝑧 ) ⊆ 𝑧 ) ↔ ( ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ⊆ 𝑧 ∧ 𝑥 ⊆ 𝑧 ∧ ( 𝑧 ∘ 𝑧 ) ⊆ 𝑧 ) ) |

77 | 76 | abbii | ⊢ { 𝑧 ∣ ( ( 𝑥 ∪ ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ) ⊆ 𝑧 ∧ ( 𝑧 ∘ 𝑧 ) ⊆ 𝑧 ) } = { 𝑧 ∣ ( ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ⊆ 𝑧 ∧ 𝑥 ⊆ 𝑧 ∧ ( 𝑧 ∘ 𝑧 ) ⊆ 𝑧 ) } |

78 | 77 | inteqi | ⊢ ∩ { 𝑧 ∣ ( ( 𝑥 ∪ ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ) ⊆ 𝑧 ∧ ( 𝑧 ∘ 𝑧 ) ⊆ 𝑧 ) } = ∩ { 𝑧 ∣ ( ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ⊆ 𝑧 ∧ 𝑥 ⊆ 𝑧 ∧ ( 𝑧 ∘ 𝑧 ) ⊆ 𝑧 ) } |

79 | 78 | mpteq2i | ⊢ ( 𝑥 ∈ V ↦ ∩ { 𝑧 ∣ ( ( 𝑥 ∪ ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ) ⊆ 𝑧 ∧ ( 𝑧 ∘ 𝑧 ) ⊆ 𝑧 ) } ) = ( 𝑥 ∈ V ↦ ∩ { 𝑧 ∣ ( ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ⊆ 𝑧 ∧ 𝑥 ⊆ 𝑧 ∧ ( 𝑧 ∘ 𝑧 ) ⊆ 𝑧 ) } ) |

80 | 6 70 79 | 3eqtri | ⊢ ( 𝑥 ∈ V ↦ ∩ { 𝑦 ∣ ( 𝑥 ⊆ 𝑦 ∧ ( ( I ↾ ( dom 𝑦 ∪ ran 𝑦 ) ) ⊆ 𝑦 ∧ ( 𝑦 ∘ 𝑦 ) ⊆ 𝑦 ) ) } ) = ( 𝑥 ∈ V ↦ ∩ { 𝑧 ∣ ( ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ⊆ 𝑧 ∧ 𝑥 ⊆ 𝑧 ∧ ( 𝑧 ∘ 𝑧 ) ⊆ 𝑧 ) } ) |

81 | 1 80 | eqtr4i | ⊢ t* = ( 𝑥 ∈ V ↦ ∩ { 𝑦 ∣ ( 𝑥 ⊆ 𝑦 ∧ ( ( I ↾ ( dom 𝑦 ∪ ran 𝑦 ) ) ⊆ 𝑦 ∧ ( 𝑦 ∘ 𝑦 ) ⊆ 𝑦 ) ) } ) |